proposition: Lemma Cnorm_opp : forall z, Cnorm (-z) = Cnorm z.
proof: Proof. intros z ; unfold Cnorm, Cnorm_sqr ; destruct z as (a,b). simpl ; replace (a * a + b * b)%R with (- a * - a + - b * - b)%R by field ; reflexivity. Qed.
imports: Cbase Cpow