proposition: Lemma bridges_lemma2a : l_u_b OF (seq2set g).
proof: Proof. intros. apply (lubp (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. intro. exists (saghf g_ N[+][1]). red in |- *. intros x H0 y H1. red in H0. case H0. intro n. intro c. apply less_transitive_unfolded with (y := x). assumption. apply less_wdl with (x := g_ n). case (le_ge_dec N n). intro H2. apply leEq_less_trans with (y := g_ N[+][1]). apply shift_leEq_plus'. cut (AbsSmall [1] (g_ n[-]g_ N)). intro. elim H3. intros H4 H5. assumption. apply a. assumption. apply plus_resp_less_rht. apply Psaghf. apply le_n. intro H2. apply less_transitive_unfolded with (y := saghf g_ N). apply Psaghf. assumption. apply less_plusOne. apply eq_symmetric_unfolded. exact c. apply (pg [1]). apply pos_one. 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 (l_u_b OF (fun x : OF => {n : nat | n <= N | x[=]g_ n})). intro H1. red in H1. case H1. intro sigma. intros p. elim p. intros. cut (a[<](a[+]b) [/]TwoNZ). intro H2. case (less_cotransitive_unfolded _ a ((a[+]b) [/]TwoNZ) H2 sigma). intro c. right. case (b0 a c). intro xj. intro H5. exists xj. elim H5. intros H6 H7. case H6. intro j. intros H9 H10. red in |- *. exists j. simpl in |- *. assumption. elim H5. intros. assumption. intro. left. red in |- *. intros x H3 z H4. red in H3. case H3. intro n. intros. case (le_ge_dec N n). intro H7. rstepr (a[+](b[-]a)). apply less_transitive_unfolded with (y := sigma[+](b[-]a) [/]TwoNZ). apply shift_less_plus. apply (a1 (g_ N)). exists N. apply le_n. apply eq_reflexive_unfolded. apply shift_minus_less. apply less_leEq_trans with (y := x). assumption. apply leEq_wdl with (x := g_ n). apply shift_leEq_plus'. cut (AbsSmall ((b[-]a) [/]TwoNZ) (g_ n[-]g_ N)). intro H8. elim H8. intros H9 H10. assumption. apply a0. assumption. apply eq_symmetric_unfolded. assumption. apply shift_plus_less. rstepr ((a[+]b) [/]TwoNZ). assumption. intro. rstepr (a[+](b[-]a)). apply less_transitive_unfolded with (y := sigma[+](b[-]a) [/]TwoNZ). apply shift_less_plus. apply (a1 x). exists n. assumption. assumption. apply shift_minus_less. apply less_transitive_unfolded with (y := x). assumption. apply shift_less_plus'. astepl ([0]:OF). apply pos_div_two. apply shift_zero_less_minus. assumption. apply shift_plus_less. rstepr ((a[+]b) [/]TwoNZ). assumption. apply plus_cancel_less with (z := [--]a). rstepl ([0]:OF). rstepr ((b[-]a) [/]TwoNZ). apply pos_div_two. apply shift_zero_less_minus. assumption. apply bridges_lemma1a 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). apply (pg ((b[-]a) [/]TwoNZ)). apply pos_div_two. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.Bridges_LUB