proposition: Lemma mult_CC_contin : forall (x y : CC) (e : IR), [0] [<] e -> {c : IR | [0] [<] c | {d : IR | [0] [<] d | forall x' y', AbsCC (x[-]x') [<=] c -> AbsCC (y[-]y') [<=] d -> AbsCC (x[*]y[-]x'[*]y') [<=] e}}.
proof: Proof. do 3 intro. intro H. cut ([0] [<] e [/]TwoNZ). intro H0. elim (estimate_absCC x). intro X. intros H1 H2. elim (estimate_absCC y). intro Y. intros H3 H4. cut (Y[#][0]). intro H5. exists (e [/]TwoNZ[/] Y[//]H5). apply div_resp_pos. auto. auto. cut ([0] [<] X[+](e [/]TwoNZ[/] Y[//]H5)). intro. cut (X[+](e [/]TwoNZ[/] Y[//]H5)[#][0]). intro H7. exists (e [/]TwoNZ[/] X[+](e [/]TwoNZ[/] Y[//]H5)[//]H7). apply div_resp_pos. auto. auto. intros. apply leEq_wdl with (AbsCC ((x[-]x')[*]y[+]x'[*](y[-]y'))). apply leEq_transitive with (AbsCC ((x[-]x')[*]y)[+]AbsCC (x'[*](y[-]y'))). apply triangle. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). apply plus_resp_leEq_both. apply leEq_wdr with ((e [/]TwoNZ[/] Y[//]H5)[*]Y). apply mult_absCC; auto. rational. apply leEq_wdr with ((X[+](e [/]TwoNZ[/] Y[//]H5))[*] (e [/]TwoNZ[/] X[+](e [/]TwoNZ[/] Y[//]H5)[//]H7)). apply mult_absCC; auto. apply leEq_wdl with (AbsCC (x[+](x'[-]x))). apply leEq_transitive with (AbsCC x[+]AbsCC (x'[-]x)). apply triangle. apply plus_resp_leEq_both. auto. astepl (AbsCC [--](x'[-]x)). apply leEq_wdl with (AbsCC (x[-]x')). auto. apply AbsCC_wd. rational. apply AbsCC_wd. rational. rational. apply AbsCC_wd. rational. apply Greater_imp_ap. auto. apply plus_resp_pos; auto. apply div_resp_pos; auto. apply Greater_imp_ap. auto. apply pos_div_two. auto. Qed.
imports: CoRN.fta.CC_Props