---

Step * of Lemma qmin-symmetry

∀[x,y:ℚ].  (qmin(x;y) = qmin(y;x) ∈ ℚ)
BY
{ (Auto THEN Unfold `qmin` 0 THEN RepeatFor 2 ((SplitOnConclITE THENA Auto)) THEN Auto) }

1
.....falsecase..... 
1. x : ℚ
2. y : ℚ
3. ¬(x ≤ y)
4. ¬(y ≤ x)
⊢ y = x ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbQ{}].    (qmin(x;y)  =  qmin(y;x))


By

---

Latex:
(Auto  THEN  Unfold  `qmin`  0  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))  THEN  Auto)

---

Home Index