proposition: Lemma AbsCC_IR : forall x : IR, [0] [<=] x -> AbsCC (cc_IR x) [=] x.
proof: Proof. intros. unfold AbsCC in |- *. change (sqrt (x[^]2[+][0][^]2) (cc_abs_aid _ x [0]) [=] x) in |- *. apply eq_transitive_unfolded with (sqrt (x[^]2) (sqr_nonneg _ x)). apply sqrt_wd. rational. apply sqrt_to_nonneg. auto. Qed.
imports: CoRN.complex.CComplex