Step * of Lemma rmul-rdiv-cancel4

[a,b,c:ℝ].  ((b/a) c) (b c) supposing a ≠ r0
BY
Auto }


Latex:


Latex:
\mforall{}[a,b,c:\mBbbR{}].    ((b/a)  *  a  *  c)  =  (b  *  c)  supposing  a  \mneq{}  r0


By


Latex:
Auto




Home Index