---

Step * of Lemma modulus_base

∀[m:ℕ+]. ∀[a:ℕm].  (a mod m ~ a)
BY
{ (Auto
   THEN Unfold `modulus` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstLemma `rem_bounds_1` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
   THEN AutoSplit) }

1
1. m : ℕ+
2. a : ℕm
3. ¬a rem m < 0
4. (0 ≤ (a rem m)) ∧ a rem m < m
⊢ (a rem m) = a ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[a:\mBbbN{}m].    (a  mod  m  \msim{}  a)


By

---

Latex:
(Auto
  THEN  Unfold  `modulus`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  AutoSplit)

---

Home Index