---

Step * 1 1 1 1 1 of Lemma radd-positive-implies


1. v : ℤ
2. v ≤ 8
3. v = (((v ÷ 4) * 4) + (v rem 4)) ∈ ℤ
4. 4 < v ÷ 4
⊢ False
BY
{ ((InstLemma `rem_bounds_absval` [⌜4⌝;⌜v⌝]⋅ THEN Auto)
   THEN (RWO "absval_strict_ubound" (-1) THENA Auto)
   THEN (Subst' |4| ~ 4 -1 THENM D -1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  \mBbbZ{}
2.  v  \mleq{}  8
3.  v  =  (((v  \mdiv{}  4)  *  4)  +  (v  rem  4))
4.  4  <  v  \mdiv{}  4
\mvdash{}  False


By

---

Latex:
((InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (RWO  "absval\_strict\_ubound"  (-1)  THENA  Auto)
  THEN  (Subst'  |4|  \msim{}  4  -1  THENM  D  -1)
  THEN  Auto)

---

Home Index