proposition: Lemma complexe_pol_argument : forall (z : C) (r a : R), z <> zeroC -> z = cons_pol r a -> argument z = image_angle a.
proof: Proof. intros. rewrite H0; rewrite complexe_polaire_argument; auto. rewrite <- (complexe_pol_module (z:=z) (r:=r) (a:=a)); auto with geo. Qed.