proposition: Lemma fun_Lim_seq_mult' : forall H H', conv_fun_seq' a b Hab (fun n => f n{*}g n) (F{*}G) H H'.
proof: Proof. intros. set (nF := Norm_Funct contF) in *. set (nG := Norm_Funct contG) in *. red in |- *; intros. set (ee := Min e [1]) in *. cut ([0] [<] ee); intros. set (eg := ee [/]ThreeNZ[/] _[//]max_one_ap_zero nF) in *. set (ef := ee [/]ThreeNZ[/] _[//]max_one_ap_zero nG) in *. cut ([0] [<] eg). intro Heg. cut ([0] [<] ef). intro Hef. elim (convF _ Hef); intros NF HNF; clear convF. elim (convG _ Heg); intros NG HNG; clear convG. cut (NF <= Nat.max NF NG); [ intro | apply Nat.le_max_l ]. cut (NG <= Nat.max NF NG); [ intro | apply Nat.le_max_r ]. exists (Nat.max NF NG); intros. apply leEq_transitive with ee. 2: unfold ee in |- *; apply Min_leEq_lft. apply leEq_wdl with (AbsIR (Part _ _ (incf n x Hx) [*]Part _ _ (incg n x Hx) [-] Part _ _ (incF x Hx) [*]Part _ _ (incG x Hx))). 2: apply AbsIR_wd; simpl in |- *; algebra. apply leEq_wdl with (AbsIR (Part _ _ (incF x Hx) [*] (Part _ _ (incg n x Hx) [-]Part _ _ (incG x Hx)) [+] (Part _ _ (incf n x Hx) [-]Part _ _ (incF x Hx)) [*] (Part _ _ (incg n x Hx) [-]Part _ _ (incG x Hx)) [+] Part _ _ (incG x Hx) [*] (Part _ _ (incf n x Hx) [-]Part _ _ (incF x Hx)))). 2: apply AbsIR_wd; simpl in |- *; rational. rstepr (ee [/]ThreeNZ[+]ee [/]ThreeNZ[+]ee [/]ThreeNZ). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (Max nF [1][*]AbsIR (Part _ _ (incg n x Hx) [-]Part _ _ (incG x Hx))). apply mult_resp_leEq_rht. apply leEq_transitive with nF. unfold nF in |- *; apply norm_bnd_AbsIR; assumption. apply lft_leEq_Max. apply AbsIR_nonneg. eapply shift_mult_leEq'. apply pos_max_one. unfold eg in HNG; unfold incg in |- *; apply HNG; apply Nat.le_trans with (Nat.max NF NG); auto. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (ee [/]ThreeNZ[*]ee [/]ThreeNZ). 2: astepr (ee [/]ThreeNZ[*][1]); apply mult_resp_leEq_lft. apply mult_resp_leEq_both; try apply AbsIR_nonneg. eapply leEq_transitive. unfold incf in |- *; apply HNF; apply Nat.le_trans with (Nat.max NF NG); auto. unfold ef in |- *. apply shift_div_leEq. apply pos_max_one. astepl (ee [/]ThreeNZ[*][1]); apply mult_resp_leEq_lft. apply rht_leEq_Max. apply less_leEq; apply shift_less_div; astepl ZeroR; [ apply pos_three | assumption ]. eapply leEq_transitive. unfold incg in |- *; apply HNG; apply Nat.le_trans with (Nat.max NF NG); auto. unfold eg in |- *. apply shift_div_leEq. apply pos_max_one. astepl (ee [/]ThreeNZ[*][1]); apply mult_resp_leEq_lft. apply rht_leEq_Max. apply less_leEq; apply shift_less_div; astepl ZeroR; [ apply pos_three | assumption ]. apply shift_div_leEq. apply pos_three. astepr (Three:IR). unfold ee in |- *; apply leEq_transitive with OneR. apply Min_leEq_rht. apply less_leEq; apply one_less_three. apply less_leEq; apply shift_less_div. apply pos_three. astepl ZeroR; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply leEq_transitive with (Max nG [1][*]AbsIR (Part _ _ (incf n x Hx) [-]Part _ _ (incF x Hx))). apply mult_resp_leEq_rht. apply leEq_transitive with nG. unfold nG in |- *; apply norm_bnd_AbsIR; assumption. apply lft_leEq_Max. apply AbsIR_nonneg. eapply shift_mult_leEq'. apply pos_max_one. unfold ef in HNF; unfold incf in |- *; apply HNF; apply Nat.le_trans with (Nat.max NF NG); auto. unfold ef in |- *. apply div_resp_pos. apply pos_max_one. apply shift_less_div; astepl ZeroR; [ apply pos_three | assumption ]. unfold eg in |- *. apply div_resp_pos. apply pos_max_one. apply shift_less_div; astepl ZeroR; [ apply pos_three | assumption ]. unfold ee in |- *; apply less_Min. assumption. apply pos_one. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval