---

Step * of Lemma modulus-is-rem

∀[a:ℕ]. ∀[n:ℤ-o].  (a mod n ~ a rem n)
BY
{ (Auto
   THEN Unfold `modulus` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (AutoSplit
         THEN ((Decide 0 < n THEN Auto)
               THENL [(InstLemma `rem_bounds_1` [⌜a⌝;⌜n⌝]⋅ THENA Auto)
                     ; (InstLemma `rem_bounds_4` [⌜a⌝;⌜n⌝]⋅ THENA Auto)]
              )
         )
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  mod  n  \msim{}  a  rem  n)


By

---

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

---

Home Index