---

Step * of Lemma ndiff_ann_l

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

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}].  ((0  --  a)  =  0)


By

---

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

---

Home Index