proposition: Lemma Cauchy_Darboux_Seq : Cauchy_prop integral_seq.
proof: Proof. red in |- *; intros e He. set (e' := e[/] _[//]mult_resp_ap_zero _ _ _ (two_ap_zero _) (max_one_ap_zero (b[-]a))) in *. cut ([0] [<] e'). intro He'. set (d := proj1_sig2T _ _ _ (contF' e' He')) in *. generalize (proj2b_sig2T _ _ _ (contF' e' He')); generalize (proj2a_sig2T _ _ _ (contF' e' He')); fold d in |- *; intros H0 H1. set (N := ProjT1 (Archimedes (b[-]a[/] _[//]pos_ap_zero _ _ H0))) in *. exists N; intros. apply AbsIR_imp_AbsSmall. apply leEq_transitive with (Two[*]e'[*] (b[-]a)). rstepr (e'[*] (b[-]a) [+]e'[*] (b[-]a)). unfold integral_seq in |- *. elim (even_partition_refinement _ _ Hab _ _ (O_S m) (O_S N)). intros w Hw. elim Hw; clear Hw; intros Hw H2 H3. unfold Even_Partition_Sum in |- *. unfold I in |- *; apply second_refinement_lemma with (a := a) (b := b) (F := F) (contF := contF) (Q := Even_Partition Hab w Hw) (He := He') (He' := He'). assumption. assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply even_partition_Mesh. apply shift_div_leEq. apply pos_nring_S. apply shift_leEq_mult' with (pos_ap_zero _ _ H0). assumption. apply leEq_transitive with (nring (R:=IR) N). exact (ProjT2 (Archimedes (b[-]a[/] d[//]pos_ap_zero _ _ H0))). apply nring_leEq; apply le_S; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply even_partition_Mesh. apply shift_div_leEq. apply pos_nring_S. apply shift_leEq_mult' with (pos_ap_zero _ _ H0). assumption. apply leEq_transitive with (nring (R:=IR) N). exact (ProjT2 (Archimedes (b[-]a[/] d[//]pos_ap_zero _ _ H0))). apply nring_leEq; apply Nat.le_succ_diag_r. unfold e' in |- *. rstepl (e[*] (b[-]a) [/] _[//]max_one_ap_zero (b[-]a)). apply shift_div_leEq. apply pos_max_one. apply mult_resp_leEq_lft. apply lft_leEq_Max. apply less_leEq; assumption. unfold e' in |- *. apply div_resp_pos. apply mult_resp_pos. apply pos_two. apply pos_max_one. assumption. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)