proposition: Lemma AbsCC_pos : forall x : CC, x [#] [0] -> [0] [<] AbsCC x.
proof: Proof. intro. elim x. intros x1 x2. unfold AbsCC in |- *. simpl in |- *. unfold cc_ap in |- *. simpl in |- *. intros H. change ([0] [<] sqrt (x1[^]2[+]x2[^]2) (cc_abs_aid _ x1 x2)) in |- *. apply power_cancel_less with 2. apply sqrt_nonneg. astepl ZeroR. astepr (x1[^]2[+]x2[^]2). elim H; clear H; intros. apply plus_resp_pos_nonneg. apply pos_square. auto. apply sqr_nonneg. apply plus_resp_nonneg_pos. apply sqr_nonneg. apply pos_square. auto. Qed.
imports: CoRN.complex.CComplex