proposition: Lemma mult_contin : forall x y e : R, [0] [<] e -> {c : R | [0] [<] c | {d : R | [0] [<] d | forall x' y' : R, AbsSmall c (x[-]x') -> AbsSmall d (y[-]y') -> AbsSmall e (x[*]y[-]x'[*]y')}}.
proof: Proof. intros x y e H. set (e2 := e [/]TwoNZ) in *. cut ([0] [<] e2). intro H0. 2: unfold e2 in |- *; apply pos_div_two; auto. elim (estimate_abs x). intro X. intros H1a H1b. elim (estimate_abs y). intro Y. intros H2 H3. cut (Y [#] [0]). intro H4. set (eY := e2[/] Y[//]H4) in *; exists eY. unfold eY in |- *. apply div_resp_pos. auto. auto. cut ([0] [<] X[+]eY). intro H5. cut (X[+]eY [#] [0]). intro H6. exists (e2[/] X[+]eY[//]H6). apply div_resp_pos. auto. auto. intros. apply AbsSmall_wdr_unfolded with ((x[-]x')[*]y[+]x'[*](y[-]y')). apply AbsSmall_eps_div_two. apply AbsSmall_wdl_unfolded with ((e [/]TwoNZ[/] Y[//]H4)[*]Y). apply mult_AbsSmall; auto. rational. apply AbsSmall_wdl_unfolded with ((X[+](e [/]TwoNZ[/] Y[//]H4))[*] (e [/]TwoNZ[/] X[+](e [/]TwoNZ[/] Y[//]H4)[//]H6)). apply mult_AbsSmall; auto. apply AbsSmall_wdr_unfolded with (x[+](x'[-]x)). apply AbsSmall_plus; auto. apply AbsSmall_minus. auto. rational. rational. rational. apply Greater_imp_ap. auto. apply plus_resp_pos; auto. unfold eY in |- *; apply div_resp_pos; auto. apply Greater_imp_ap. auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)