proposition: Lemma CS_seq_mult : Cauchy_prop (fun n => f n[*]g n).
proof: Proof. red in |- *; intros e He. elim (CS_seq_bounded f Hf); intros Mf HMf H. elim (CS_seq_bounded g Hg); intros Mg HMg H'. elim H; clear H; intros Nf HNf. elim H'; clear H'; intros Ng HNg. set (Mf_ap_zero := pos_ap_zero _ _ HMf) in *. set (Mg_ap_zero := pos_ap_zero _ _ HMg) in *. set (ef := e[/] _[//]mult_resp_ap_zero _ _ _ (twelve_ap_zero _) Mf_ap_zero) in *. set (eg := e[/] _[//]mult_resp_ap_zero _ _ _ (twelve_ap_zero _) Mg_ap_zero) in *. cut ([0] [<] ef); [ intro Hef | unfold ef in |- *; apply div_resp_pos; try apply mult_resp_pos; auto; apply pos_twelve ]. cut ([0] [<] eg); [ intro Heg | unfold eg in |- *; apply div_resp_pos; try apply mult_resp_pos; auto; apply pos_twelve ]. elim (Hf eg Heg); intros Pf HPf. elim (Hg ef Hef); intros Pg HPg. set (N := Nat.max (Nat.max Nf Pf) (Nat.max Ng Pg)) in *; exists N; intros m Hm. rstepr ((f m[-]f Pf[+][--](f N[-]f Pf))[*]g m[+] (g m[-]g Pg[+][--](g N[-]g Pg))[*]f N). apply AbsSmall_wdl_unfolded with (Three[*]((eg[+]eg)[*]Mg)[+]Three[*]((ef[+]ef)[*]Mf)). 2: unfold eg, ef in |- *; rational. apply AbsSmall_plus; apply AbsSmall_mult; try apply AbsSmall_plus; try apply inv_resp_AbsSmall. apply HPf; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith. apply HPf; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith. apply HNg; auto; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith. apply HPg; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith. apply HPg; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith. apply HNf; auto; apply Nat.le_trans with N; auto; unfold N in |- *; eauto with arith. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)