---

Step * of Lemma zero-add-base

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  SqReasoning  THEN  ThinTrivial)

---

Home Index