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