---

Step * of Lemma rem_eq_args

∀[a:ℕ+]. ((a rem a) = 0 ∈ ℤ)
BY
{ ((UnivCD THENA Auto) THEN RWO "rem_rec_case rem_base_case" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}\msupplus{}].  ((a  rem  a)  =  0)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "rem\_rec\_case  rem\_base\_case"  0  THEN  Auto)

---

Home Index