proposition: Lemma Cinv_argument : forall z : C, z <> zeroC -> argument (Cinv z) = opp (argument z).
proof: Proof. intros. cut (Cinv z <> zeroC); intros; auto with geo. cut (plus (argument z) (argument (Cinv z)) = image_angle 0); intros. apply opp_angle; auto. rewrite <- argument_oneC. rewrite <- Cmult_argument; auto with geo. rewrite Cinv_def; auto with geo. Qed.