---

Step * 3 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_3_to_1`) 0)⋅ THENA 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.  \mneg{}-1  <  b
5.  -a  <  -b
\mvdash{}  (a  rem  b)  =  a


By

---

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

---

Home Index