proposition: Lemma CS_seq_diagonal : forall a : CauchySeq R_COrdField', Cauchy_prop (fun m => let b := (CS_seq _ a m) in CS_seq F b (T b m)).
proof: Proof. intros. unfold Cauchy_prop in |- *. case a. intros a_ pa. intros. simpl in |- *. unfold Cauchy_prop in pa. cut (e [#] [0]). intro H0. cut {n : nat | (Twelve[/] e[//]H0) [-][1] [<] nring n}. intro H1. case H1. intros M H2. cut {N : nat | forall m : nat, N <= m -> AbsSmall (inject_Q e [/]SixNZ) (a_ m[-]a_ N)}. intro H3. case H3. intros N H4. exists (Nat.max N M). intros. apply ing_cancel_AbsSmall. rstepl (inject_Q e [/]ThreeNZ[+]inject_Q e [/]ThreeNZ[+]inject_Q e [/]ThreeNZ). rstepr (inject_Q (CS_seq F (a_ m) (T (a_ m) m)) [-]a_ m[+] (a_ (Nat.max N M) [-] inject_Q (CS_seq F (a_ (Nat.max N M)) (T (a_ (Nat.max N M)) (Nat.max N M)))) [+] (a_ m[-]a_ (Nat.max N M))). apply AbsSmall_plus. apply AbsSmall_plus. astepl (inject_Q (e [/]ThreeNZ)). apply AbsSmall_leEq_trans with (R := R_COrdField') (e1 := inject_Q (Four[*]one_div_succ m)). apply ing_le. apply leEq_transitive with (y := Four[*]one_div_succ (R:=F) M). apply mult_resp_leEq_lft. apply one_div_succ_resp_leEq. eauto with arith. apply less_leEq. apply pos_four. apply mult_cancel_leEq with (R := F) (z := (nring M[+][1]) [*] (Three:F)). apply mult_resp_pos. apply less_transitive_unfolded with (F := F) (y := Twelve[/] e[//]H0). apply mult_cancel_less with (R := F) (z := e). assumption. rstepl ([0]:F). rstepr (Twelve:F). apply nring_pos. apply Nat.lt_0_succ. apply plus_cancel_less with (R := F) (z := [--] ([1]:F)). rstepl ((Twelve[/] e[//]H0) [-][1]). rstepr (nring (R:=F) M). exact H2. apply nring_pos. apply Nat.lt_0_succ. unfold one_div_succ in |- *. unfold Snring in |- *. change (Four[*] ([1][/] nring M[+][1][//]nringS_ap_zero F M) [*] ((nring M[+][1]) [*]Three) [<=] e [/]ThreeNZ[*] ((nring M[+][1]) [*]Three)) in |- *. rstepl (Twelve:F). rstepr (e[*] (nring M[+][1])). apply mult_cancel_leEq with (R := F) (z := [1][/] e[//]H0). apply recip_resp_pos. assumption. rstepr (nring (R:=F) M[+][1]). apply plus_cancel_leEq_rht with (R := F) (z := [--] ([1]:F)). rstepl ((Twelve[/] e[//]H0) [-][1]). rstepr (nring (R:=F) M). apply less_leEq; exact H2. apply expand_Q_R_2 with (x := a_ m) (e := Four[*]one_div_succ (R:=F) m) (N := T (a_ m) m). apply mult_resp_pos. apply pos_four. apply one_div_succ_pos. intros. rstepl (one_div_succ (R:=F) m). apply modulus_property_2. assumption. apply eq_symmetric_unfolded. apply ing_div_three. astepl (inject_Q (e [/]ThreeNZ)). apply AbsSmall_leEq_trans with (R := R_COrdField') (e1 := inject_Q (Four[*]one_div_succ (R:=F) M)). apply less_leEq. apply ing_lt. apply mult_cancel_less with (R := F) (z := (nring M[+][1]) [*] (Three:F)). apply mult_resp_pos. apply less_transitive_unfolded with (F := F) (y := Twelve[/] e[//]H0). apply mult_cancel_less with (R := F) (z := e). assumption. rstepl ([0]:F). rstepr (Twelve:F). apply nring_pos. apply Nat.lt_0_succ. apply plus_cancel_less with (R := F) (z := [--] ([1]:F)). rstepl ((Twelve[/] e[//]H0) [-][1]). rstepr (nring (R:=F) M). exact H2. apply pos_three. unfold one_div_succ in |- *. unfold Snring in |- *. change (Four[*] ([1][/] nring M[+][1][//]nringS_ap_zero F M) [*] ((nring M[+][1]) [*]Three) [<] e [/]ThreeNZ[*] ((nring M[+][1]) [*]Three)) in |- *. rstepl (Twelve:F). rstepr (e[*] (nring M[+][1])). apply mult_cancel_less with (R := F) (z := [1][/] e[//]H0). apply recip_resp_pos. assumption. rstepr (nring (R:=F) M[+][1]). apply plus_cancel_less with (R := F) (z := [--] ([1]:F)). rstepl ((Twelve[/] e[//]H0) [-][1]). rstepr (nring (R:=F) M). exact H2. apply AbsSmall_minus. apply expand_Q_R_2 with (x := a_ (Nat.max N M)) (e := Four[*]one_div_succ (R:=F) M) (N := T (a_ (Nat.max N M)) (Nat.max N M)). apply mult_resp_pos. apply pos_four. apply one_div_succ_pos. intros. rstepl (one_div_succ (R:=F) M). apply AbsSmall_leEq_trans with (R := F) (e1 := one_div_succ (R:=F) (Nat.max N M)). apply one_div_succ_resp_leEq. auto with arith. apply modulus_property_2. assumption. apply eq_symmetric_unfolded. apply ing_div_three. rstepl (inject_Q e [/]SixNZ[+]inject_Q e [/]SixNZ). rstepr (a_ m[-]a_ N[+] (a_ N[-]a_ (Nat.max N M))). apply AbsSmall_plus. apply H4; eauto with arith. apply AbsSmall_minus. apply H4; eauto with arith. apply pa. apply mult_cancel_less with (R := R_COrdField') (z := Six:R_COrdField'). apply pos_six. rstepl ([0]:R_COrdField'). rstepr (inject_Q e). change (inject_Q ([0]:F) [<] inject_Q e) in |- *. apply ing_lt. assumption. apply F_is_archemaedian. apply Greater_imp_ap. assumption. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals