---

Step * of Lemma ndiff_inv

∀[a:ℕ]. ∀[b:ℤ].  (((a + b) -- b) = a ∈ ℤ)
BY
{ (RepUR ``ndiff imax`` 0
   THEN (UnivCD THENA Auto)
   THEN Repeat (CallByValueReduce 0)
   THEN Auto
   THEN Repeat (AutoSplit)) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[b:\mBbbZ{}].    (((a  +  b)  --  b)  =  a)


By

---

Latex:
(RepUR  ``ndiff  imax``  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Repeat  (CallByValueReduce  0)
  THEN  Auto
  THEN  Repeat  (AutoSplit))

---

Home Index