Step * of Lemma radd-rminus-assoc

[x,y:ℝ].  (((x -(x) y) y) ∧ ((-(x) y) y))
BY
RepeatFor ((RWO "radd-assoc radd-rminus-both.1 radd-rminus-both.2 radd-zero-both.2" 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