proposition: Lemma egalite_cart_pol : forall x y r a : R, r <> 0 -> module (cons_cart x y) = r -> argument (cons_cart x y) = image_angle a :>AV -> cons_cart x y = cons_pol r a :>C.
proof: Proof. intros. rewrite <- (forme_polaire_def (z:=cons_cart x y) (r:=r) (a:=a)); auto with geo. apply nonzero_module. rewrite H0; auto. Qed.