---

Step * 1 of Lemma qmin-eq-iff-1


1. q : ℚ
2. r : ℚ
3. (r ≤ q) ⇒ (q = r ∈ ℚ)
4. (q ≤ r) ⇒ (q = q ∈ ℚ)
⊢ q ≤ r
BY
{ (SupposeNot THEN (FLemma `not-qle` [-1] THENA Auto) THEN D 3 THEN Auto) }

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  r  :  \mBbbQ{}
3.  (r  \mleq{}  q)  {}\mRightarrow{}  (q  =  r)
4.  (q  \mleq{}  r)  {}\mRightarrow{}  (q  =  q)
\mvdash{}  q  \mleq{}  r


By

---

Latex:
(SupposeNot  THEN  (FLemma  `not-qle`  [-1]  THENA  Auto)  THEN  D  3  THEN  Auto)

---

Home Index