proposition: Lemma bridges_lemma2b : g_l_b OF (seq2set g).
proof: Proof. intros. apply (glbp (seq2set g)). exists (g_ 0). red in |- *. exists 0. apply eq_reflexive_unfolded. cut {N : nat | forall m : nat, N <= m -> AbsSmall [1] (g_ m[-]g_ N)}. intro H. case H. intro N. intros. exists (kaf g_ N[-][1]). red in |- *. intros x H0 z H1. case H0. intro n. intros c. apply less_wdr with (y := g_ n). case (le_ge_dec N n). intro. apply less_leEq_trans with (y := g_ N[-][1]). apply less_transitive_unfolded with (y := kaf g_ N[-][1]). assumption. apply minus_resp_less. apply Pkaf. apply le_n. apply plus_cancel_leEq_rht with (z := [--](g_ N)). rstepl ([--]([1]:OF)). astepr (g_ n[-]g_ N). cut (AbsSmall [1] (g_ n[-]g_ N)). intro. elim H2. intros. assumption. apply a. assumption. intro. apply less_transitive_unfolded with (y := kaf g_ N[-][1]). assumption. apply less_transitive_unfolded with (y := kaf g_ N). apply plus_cancel_less with (z := [1]:OF). astepl (kaf g_ N). apply less_plusOne. apply Pkaf. assumption. apply eq_symmetric_unfolded. exact c. apply (pg [1]). apply pos_one. intros x y H H0. red in |- *. red in H0. case H0. intro n. intros. exists n. apply eq_transitive_unfolded with (y := x). apply eq_symmetric_unfolded. assumption. assumption. intros a b. intro. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((b[-]a) [/]TwoNZ) (g_ m[-]g_ N)}. intro H0. case H0. intro N. intros. cut (g_l_b OF (fun x : OF => {n : nat | n <= N | x[=]g_ n})). intro H1. red in H1. case H1. intro tau. intros p. elim p. intros. cut ((a[+]b) [/]TwoNZ[<]b). intro H2. case (less_cotransitive_unfolded _ ((a[+]b) [/]TwoNZ) b H2 tau). intro. left. red in |- *. intros x H3 z H4. red in H3. case H3. intro n. intros H7. case (le_ge_dec N n). intro. red in a1. apply less_wdr with (y := g_ n). apply less_leEq_trans with (y := g_ N[-](b[-]a) [/]TwoNZ). apply shift_less_minus. apply (a1 (g_ N)). exists N. apply le_n. apply eq_reflexive_unfolded. apply less_transitive_unfolded with (y := (a[+]b) [/]TwoNZ). apply shift_plus_less. rstepr a. assumption. assumption. cut (AbsSmall ((b[-]a) [/]TwoNZ) (g_ n[-]g_ N)). intro H8. elim H8. intros H9 H10. apply shift_minus_leEq. apply shift_leEq_plus'. apply inv_cancel_leEq. rstepr (g_ n[-]g_ N). assumption. apply a0. assumption. apply eq_symmetric_unfolded. assumption. intro. apply less_transitive_unfolded with (y := z[+](b[-]a) [/]TwoNZ). apply plus_cancel_less with (z := [--]z). rstepl ([0]:OF). rstepr ((b[-]a) [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. apply (a1 x). exists n. assumption. assumption. apply less_transitive_unfolded with (y := (a[+]b) [/]TwoNZ). apply shift_plus_less. rstepr a. assumption. assumption. right. case (b0 b c). intro xj. intro p0. exists xj. elim p0. intros H6 H7. case H6. intro j. intros H9 H10. red in |- *. exists j. simpl in |- *. assumption. elim p0. intros. assumption. apply plus_cancel_less with (z := [--]((a[+]b) [/]TwoNZ)). rstepl ([0]:OF). rstepr ((b[-]a) [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. apply bridges_lemma1b with (P := P N) (is_finite_P := fin_is_fin N). intros. unfold P in |- *. exists t. rewrite <- (card_fin N). assumption. apply (finite_seq N). unfold P in |- *. intros x H1 z H2. case H2. intro n. intros. exists n. intros. assumption. apply eq_transitive_unfolded with (y := x). apply eq_symmetric_unfolded. assumption. assumption. apply (pg ((b[-]a) [/]TwoNZ)). apply pos_div_two. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.Bridges_LUB