---

Step * of Lemma monus_of_add

n,a:.  ((n + a--a) ~ n)
BY
{ (Unfold `monus` 0 THEN Auto THEN AutoSplit) }

1
1. n : @i
2. a : @i
3. (n + a) < a
 0 = n


\mforall{}n,a:\mBbbN{}.    ((n  +  a--a)  \msim{}  n)


By

(Unfold  `monus`  0  THEN  Auto  THEN  AutoSplit)



Home Index