proposition: Lemma argument_Conj2 : forall z : C, z <> zeroC -> argument (Conj z) = opp (argument z).
proof: Proof. intros. elim existence_argument with (z := z); [ intros a H7; try clear existence_argument; try exact H7 | auto with geo ]. rewrite (argument_Conj (z:=z) (a:=a)); auto with geo. rewrite H7; auto with geo. Qed.