proposition: Lemma forme_polaire_Conj : forall (z : C) (r a : R), z <> zeroC -> z = cons_pol r a -> Conj z = cons_pol r (- a).
proof: Proof. intros. apply forme_polaire_def; auto with geo. rewrite module_Conj; auto. eauto with geo. apply argument_Conj; auto with geo. eauto with geo. Qed.