---

Step * of Lemma div_mono1

∀[i,k:ℕ].  (i ÷ k < i) supposing (1 < k and 0 < i)
BY
{ (Auto THEN (Decide i < k THENA Auto)) }

1
1. i : ℕ
2. k : ℕ
3. 0 < i
4. 1 < k
5. i < k
⊢ i ÷ k < i

2
1. i : ℕ
2. k : ℕ
3. 0 < i
4. 1 < k
5. ¬i < k
⊢ i ÷ k < i

---

Latex:

---

Latex:
\mforall{}[i,k:\mBbbN{}].    (i  \mdiv{}  k  <  i)  supposing  (1  <  k  and  0  <  i)


By

---

Latex:
(Auto  THEN  (Decide  i  <  k  THENA  Auto))

---

Home Index