proposition: Lemma unicite_forme_polaire_nonzero : forall (z : C) (r a r' a' : R), z <> zeroC -> z = cons_pol r a -> z = cons_pol r' a' -> r = r' /\ image_angle a = image_angle a'.
proof: Proof. intros. split. rewrite <- (complexe_pol_module (z:=z) (r:=r) (a:=a)); eauto with geo. rewrite <- (complexe_pol_argument (z:=z) (r:=r) (a:=a)); eauto with geo. Qed.