---

Step * 2 of Lemma div_mono1


1. i : ℕ
2. k : ℕ
3. 0 < i
4. 1 < k
5. ¬i < k
⊢ i ÷ k < i
BY
{ (((InstLemma `div_rem_sum` [⌜i⌝; ⌜k⌝])⋅ THENA Auto) THEN ((InstLemma `rem_bounds_1`[⌜i⌝; ⌜k⌝])⋅ THENA Auto)) }

1
1. i : ℕ
2. k : ℕ
3. 0 < i
4. 1 < k
5. ¬i < k
6. i = (((i ÷ k) * k) + (i rem k)) ∈ ℤ
7. (0 ≤ (i rem k)) ∧ i rem k < k
⊢ i ÷ k < i

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  0  <  i
4.  1  <  k
5.  \mneg{}i  <  k
\mvdash{}  i  \mdiv{}  k  <  i


By

---

Latex:
(((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}k\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `rem\_bounds\_1`[\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}k\mkleeneclose{}])\mcdot{}  THENA  Auto)
  )

---

Home Index