---

Step * 2 of Lemma rem_base_case_z


1. a : ℤ
2. ¬-1 < a
3. b : ℤ-o
4. -1 < b
5. -a < b
⊢ (a rem b) = a ∈ ℤ
BY
{ TACTIC:((RWH (LemmaC `rem_2_to_1`) 0)⋅ THEN Auto THEN InstLemma `rem_base_case` [⌜-a⌝;⌜b⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  \mneg{}-1  <  a
3.  b  :  \mBbbZ{}\msupminus{}\msupzero{}
4.  -1  <  b
5.  -a  <  b
\mvdash{}  (a  rem  b)  =  a


By

---

Latex:
TACTIC:((RWH  (LemmaC  `rem\_2\_to\_1`)  0)\mcdot{}
                THEN  Auto
                THEN  InstLemma  `rem\_base\_case`  [\mkleeneopen{}-a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                THEN  Auto)

---

Home Index