---

Step * 1 of Lemma rpositive-int


1. n : ℤ
2. n@0 : ℕ+
3. 4 < 2 * n@0 * n
⊢ 0 < n
BY
{ (SupposeNot THEN InstLemma `mul_preserves_le` [⌜n⌝;⌜0⌝;⌜n@0⌝]⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  n@0  :  \mBbbN{}\msupplus{}
3.  4  <  2  *  n@0  *  n
\mvdash{}  0  <  n


By

---

Latex:
(SupposeNot  THEN  InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n@0\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index