proposition: Lemma Cdiv_argument : forall z z' : C, z <> zeroC -> z' <> zeroC -> argument (Cdiv z z') = plus (argument z) (opp (argument z')).
proof: Proof. intros. rewrite Cdiv_def; auto with geo. rewrite Cmult_argument; auto with geo. rewrite Cinv_argument; auto with geo. Qed.