proposition: Lemma bridges_lemma1b : g_l_b OF P.
proof: Proof. intros. red in |- *. cut (l_u_b OF (fun x : OF => P [--]x)). intro H. red in H. case H. intro b. intros p. elim p. intros H0 H1. exists ([--]b). split. red in |- *. red in H0. intros x H2 z H3. case (less_cotransitive_unfolded OF z [--]b H3 x). trivial. intro. elim (less_irreflexive_unfolded _ b). apply H0 with (x := [--]x) (z := b). apply (P_is_strongly_extensional x [--][--]x). algebra. assumption. apply inv_cancel_less. astepl x. assumption. intros. case (H1 [--]c'). apply inv_cancel_less. astepr c'. assumption. intro s. intros H3. elim H3. intros. exists ([--]s). split. assumption. apply inv_cancel_less. astepr s. assumption. apply (lubp (fun x : OF => P [--]x)). case P_is_inhabited. intro x. intro. exists ([--]x). apply (P_is_strongly_extensional x [--][--]x). algebra. assumption. case is_finite_P. intro N. intros. case s. intro r. intro. exists (saghf (fun n : nat => [--](r n)) N). red in |- *. intros x H z H0. apply less_transitive_unfolded with (y := x). assumption. case (s0 [--]x H). intro m. intros H1 H2. apply less_wdl with (x := [--](r m)). apply (Psaghf (fun m : nat => [--](r m))). assumption. rstepl (([0]:OF)[-]r m). rstepr (([0]:OF)[-][--]x). apply cg_minus_wd. apply eq_reflexive_unfolded. assumption. intros x y H. cut ((forall k : nat, k <= card -> [--](seq k)[<]y) or {j : nat | P (seq j) | x[<][--](seq j)}). intro H0. case H0. intro c. left. red in |- *. intros x0 H1 z H2. apply less_transitive_unfolded with (y := x0). assumption. elim (Pindeks [--]x0 H1). intros. apply less_wdl with (x := [--](seq (indeks [--]x0 H1))). apply c. assumption. rstepl (([0]:OF)[-]seq (indeks [--]x0 H1)). rstepr (([0]:OF)[-][--]x0). apply cg_minus_wd. apply eq_reflexive_unfolded. assumption. intro e. right. case e. intro j. intros H2 H3. exists ([--](seq j)). apply (P_is_strongly_extensional (seq j) [--][--](seq j)). algebra. assumption. assumption. case (bounded_quantifier_informative card) with (phi := fun k : nat => [--](seq k)[<]y) (psi := fun k : nat => x[<][--](seq k)). intros. cut (x[<][--](seq m) or [--](seq m)[<]y). intro H1. case H1. intro. right. assumption. intro. left. assumption. apply less_cotransitive_unfolded. assumption. intros. left. assumption. intro e. right. case e. intro j. intros. exists j. apply is_onto_seq_P. apply Cle_to. assumption. assumption. Qed.
imports: CoRN.reals.Bridges_LUB