proposition: Lemma Cmult_z_oneC : forall z : C, Cmult z oneC = z.
proof: Proof. intros. elim (classic (z = zeroC)); intros. rewrite H. repeat rewrite Cmult_zeroC_z; auto with geo. apply egalite_forme_polaire; auto with geo. rewrite Cmult_module; rewrite module_oneC; ring. repeat rewrite Cmult_argument; auto with geo. rewrite argument_oneC; auto with geo. Qed.