---

Step * 1 of Lemma rem_base_case_z


1. a : ℤ
2. b : ℤ-o
3. ¬-1 < b
4. -1 < a
5. a < -b
⊢ (a rem b) = a ∈ ℤ
BY
{ ((InstLemma `rem_sym` [⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN RevHypSubst' (-1) 0 THEN RWO "rem_base_case" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `rem\_sym`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0
  THEN  RWO  "rem\_base\_case"  0
  THEN  Auto)

---

Home Index