---

Step * of Lemma rem-one

No Annotations
∀[x:ℤ]. (x rem 1 ~ 0)
BY
{ (Auto THEN (Decide 0 ≤ x THENA Auto)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\mBbbZ{}].  (x  rem  1  \msim{}  0)


By

---

Latex:
(Auto  THEN  (Decide  0  \mleq{}  x  THENA  Auto))

---

Home Index