proposition: Lemma pol_complexe_argument : forall (z : C) (r a : R) (M : PO), z <> zeroC -> z = cons_pol r a -> M = image z -> cons_AV (vec O I) (vec O M) = image_angle a.
proof: Proof. intros. rewrite <- (argument_def (M:=M) (z:=z)); eauto with geo. Qed.