---

Step * of Lemma monus_le

a,b,c:.  ((a  b)  ((a--c)  (b--c)))
BY
{ (Auto THEN RepUR ``monus`` 0 THEN RepeatFor 2 (AutoSplit)) }


\mforall{}a,b,c:\mBbbN{}.    ((a  \mleq{}  b)  {}\mRightarrow{}  ((a--c)  \mleq{}  (b--c)))


By

(Auto  THEN  RepUR  ``monus``  0  THEN  RepeatFor  2  (AutoSplit))



Home Index