proposition: Lemma AbsSmall_AbsCC : forall (z : CC) (e : IR), [0] [<] e -> AbsSmall (e [/]TwoNZ) (Re z) -> AbsSmall (e [/]TwoNZ) (Im z) -> AbsCC z [<=] e.
proof: Proof. intros. unfold AbsCC in |- *. apply power_cancel_leEq with 2. auto. apply less_leEq. auto. astepl (Re z[^]2[+]Im z[^]2). rstepr ((e [/]TwoNZ) [^]2[+] (e [/]TwoNZ) [^]2[+] (e[^]2) [/]TwoNZ). astepl (Re z[^]2[+]Im z[^]2[+][0]). apply plus_resp_leEq_both. apply plus_resp_leEq_both. apply AbsSmall_sqr. auto. apply AbsSmall_sqr. auto. apply less_leEq. apply div_resp_pos. apply pos_two. apply nexp_resp_pos. auto. Qed.
imports: CoRN.complex.AbsCC Coq(Lia)