---

Step * 1 of Lemma rmin-classical-cases


1. a : ℝ
2. b : ℝ
3. ¬((rmin(a;b) = a) ∨ (rmin(a;b) = b))
⊢ False
BY
{ ((StableCases ⌜a < b⌝⋅ THENA Auto) THEN Try ((FLemma `not-rless` [-1] THENA Auto)) THEN D 3) }

1
1. a : ℝ
2. b : ℝ
3. a < b
⊢ (rmin(a;b) = a) ∨ (rmin(a;b) = b)

2
1. a : ℝ
2. b : ℝ
3. ¬(a < b)
4. b ≤ a
⊢ (rmin(a;b) = a) ∨ (rmin(a;b) = b)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  \mneg{}((rmin(a;b)  =  a)  \mvee{}  (rmin(a;b)  =  b))
\mvdash{}  False


By

---

Latex:
((StableCases  \mkleeneopen{}a  <  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Try  ((FLemma  `not-rless`  [-1]  THENA  Auto))  THEN  D  3)

---

Home Index