proposition: Theorem glbp : forall X : OF -> CProp, {x : OF | X x} -> {l : OF | is_lower_bound OF X l} -> (forall x y : OF, x[=]y -> X x -> X y) -> (forall x y : OF, x[<]y -> is_lower_bound OF X x or {s : OF | X s | s[<]y}) -> g_l_b OF X.
proof: Proof. intros X H H0 strong_extensionality_of_X. intros. red in |- *. cut (l_u_b OF (fun x : OF => X [--]x)). intro H2. red in H2. case H2. intro b. intros a. exists ([--]b). elim a. intros H3 H4. split. red in |- *. intros x H5 z H6. red in H3. case (less_cotransitive_unfolded OF z [--]b H6 x). trivial. intro. exfalso. apply (less_irreflexive_unfolded _ b). apply H3 with (x := [--]x) (z := b). apply (strong_extensionality_of_X x [--][--]x). algebra. assumption. apply inv_cancel_less. astepl x. assumption. intros. case (H4 [--]c'). apply inv_cancel_less. astepr c'. assumption. intro s. intros H6. elim H6. intros. exists ([--]s). split. assumption. apply inv_cancel_less. astepr s. assumption. apply (lubp (fun x : OF => X [--]x)). case H. intro x. intro. exists ([--]x). apply (strong_extensionality_of_X x [--][--]x). algebra. assumption. case H0. intro l. intros. exists ([--]l). red in |- *. red in i. intros. apply inv_cancel_less. astepl l. apply (leEq_geEq l [--]x). intros. apply i with (x := [--]x). assumption. assumption. apply inv_resp_less. assumption. rename X0 into H1. intros x y H2. case (H1 [--]y [--]x). apply inv_resp_less. assumption. intro. left. red in |- *. red in i. intros. apply inv_cancel_less. apply (leEq_geEq [--]y [--]x0). intros. apply i with (x := [--]x0). assumption. assumption. apply inv_resp_less. assumption. intro e. right. case e. intro s. intros. exists ([--]s). apply (strong_extensionality_of_X s [--][--]s). algebra. assumption. apply inv_cancel_less. rstepl s. assumption. Qed.
imports: CoRN.reals.Bridges_LUB