---

Step * 1 of Lemma frs-increasing-separated-common-refinement


1. p : ℝ List
2. q : ℝ List
3. frs-increasing(p)
4. frs-increasing(q)
5. frs-separated(p;q)
6. ∀sb:ℝ List
     ((∀a,b:ℝ.  ((a ∈ p) ⇒ (b ∈ sb) ⇒ ((a < b) ∨ (b < a))))
     ⇒ sorted-by(λ2x y.x < y;p)
     ⇒ sorted-by(λ2x y.x < y;sb)
     ⇒ (∃sc:ℝ List. (sorted-by(λ2x y.x < y;sc) ∧ p ⊆ sc ∧ sb ⊆ sc ∧ sc ⊆ p @ sb)))
7. a : ℝ
8. b : ℝ
9. (a ∈ p)
10. (b ∈ q)
⊢ (a < b) ∨ (b < a)
BY
{ OnMaybeHyp 5 (\h. (Unfold `frs-separated` h
                     THEN (RWW "l_all_iff" h THENA Auto)
                     THEN Fold `rneq` 0
                     THEN BHyp 5 
                     THEN Auto)) }

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}  List
2.  q  :  \mBbbR{}  List
3.  frs-increasing(p)
4.  frs-increasing(q)
5.  frs-separated(p;q)
6.  \mforall{}sb:\mBbbR{}  List
          ((\mforall{}a,b:\mBbbR{}.    ((a  \mmember{}  p)  {}\mRightarrow{}  (b  \mmember{}  sb)  {}\mRightarrow{}  ((a  <  b)  \mvee{}  (b  <  a))))
          {}\mRightarrow{}  sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;p)
          {}\mRightarrow{}  sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;sb)
          {}\mRightarrow{}  (\mexists{}sc:\mBbbR{}  List.  (sorted-by(\mlambda{}\msubtwo{}x  y.x  <  y;sc)  \mwedge{}  p  \msubseteq{}  sc  \mwedge{}  sb  \msubseteq{}  sc  \mwedge{}  sc  \msubseteq{}  p  @  sb)))
7.  a  :  \mBbbR{}
8.  b  :  \mBbbR{}
9.  (a  \mmember{}  p)
10.  (b  \mmember{}  q)
\mvdash{}  (a  <  b)  \mvee{}  (b  <  a)


By

---

Latex:
OnMaybeHyp  5  (\mbackslash{}h.  (Unfold  `frs-separated`  h
                                      THEN  (RWW  "l\_all\_iff"  h  THENA  Auto)
                                      THEN  Fold  `rneq`  0
                                      THEN  BHyp  5 
                                      THEN  Auto))

---

Home Index