---

Step * of Lemma ndiff_zero

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

1
1. a : ℤ
2. b : ℤ
3. if a - b ≤z 0 then 0 else a - b fi  = 0 ∈ ℤ
⊢ a ≤ b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].    uiff((a  --  b)  =  0;a  \mleq{}  b)


By

---

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

---

Home Index