---

Step * of Lemma ndiff_add_eq_imax

∀[a,b:ℤ].  (((a -- b) + b) = imax(a;b) ∈ ℤ)
BY
{ (Auto THEN Unfold `ndiff` 0) }

1
1. a : ℤ
2. b : ℤ
⊢ (imax(a - b;0) + b) = imax(a;b) ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `ndiff`  0)

---

Home Index