---

Step * of Lemma one-rem

∀[m:ℤ]. 1 rem m ~ 1 supposing 1 < m
BY
{ (Auto THEN (InstLemma `div_rem_sum` [⌜1⌝;⌜m⌝]⋅ THENA Auto) THEN Subst' 1 ÷ m ~ 0 -1 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[m:\mBbbZ{}].  1  rem  m  \msim{}  1  supposing  1  <  m


By

---

Latex:
(Auto  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Subst'  1  \mdiv{}  m  \msim{}  0  -1  THEN  Auto')

---

Home Index