---

Step * 1 of Lemma mod2-is-one

.....assertion..... 
1. x : ℤ
⊢ (x mod 2) = 1 ∈ ℤ ⇐⇒ ((x - 1) mod 2) = 0 ∈ ℤ
BY
{ ((InstLemma `mod2-add1` [⌜x - 1⌝]⋅ THENA Auto) THEN SplitOnHypITE -1  THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  x  :  \mBbbZ{}
\mvdash{}  (x  mod  2)  =  1  \mLeftarrow{}{}\mRightarrow{}  ((x  -  1)  mod  2)  =  0


By

---

Latex:
((InstLemma  `mod2-add1`  [\mkleeneopen{}x  -  1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  SplitOnHypITE  -1    THEN  Auto)

---

Home Index