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