---

Step * of Lemma add-zero-base

∀[x:Base]. x + 0 ~ x supposing (x)↓ ⇒ (x ∈ ℤ)
BY
{ (Auto THEN SqReasoning THEN ThinTrivial) }

1
1. x : Base
2. (x)↓
3. x ∈ ℤ
⊢ x ≤ x + 0

---

Latex:

---

Latex:
\mforall{}[x:Base].  x  +  0  \msim{}  x  supposing  (x)\mdownarrow{}  {}\mRightarrow{}  (x  \mmember{}  \mBbbZ{})


By

---

Latex:
(Auto  THEN  SqReasoning  THEN  ThinTrivial)

---

Home Index