Step
*
of Lemma
radd-rminus-assoc
∀[x,y:ℝ].  (((x + -(x) + y) = y) ∧ ((-(x) + x + y) = y))
BY
{ RepeatFor 3 ((RWO "radd-assoc radd-rminus-both.1 radd-rminus-both.2 radd-zero-both.2" 0 THEN Auto)) }
Latex:
Latex:
\mforall{}[x,y:\mBbbR{}].    (((x  +  -(x)  +  y)  =  y)  \mwedge{}  ((-(x)  +  x  +  y)  =  y))
By
Latex:
RepeatFor  3  ((RWO  "radd-assoc  radd-rminus-both.1  radd-rminus-both.2  radd-zero-both.2"  0  THEN  Auto))
Home
Index