proposition: Lemma absCC_absIR_im : forall x : CC, AbsIR (Im x) [<=] AbsCC x.
proof: Proof. intros. astepl (sqrt (Im x[^]2) (sqr_nonneg _ (Im x))). unfold AbsCC in |- *. apply power_cancel_leEq with 2. auto. apply sqrt_nonneg. astepl (Im x[^]2). astepr (Re x[^]2[+]Im x[^]2). astepl ([0][+]Im x[^]2). apply plus_resp_leEq. apply sqr_nonneg. Qed.
imports: CoRN.complex.AbsCC Coq(Lia)