proposition: Lemma argument_affixe_inversion_pole_positif : forall (k : R) (M M' : PO) (z z' : C), O <> M :>PO -> k > 0 -> z = affixe_vec (vec O M) :>C -> z' = affixe_vec (vec O M') :>C -> M' = inversion O k M :>PO -> argument z' = argument z :>AV.
proof: Proof. intros. assert (vec O M' = mult_PP (/ Rsqr (distance O M) * k) (vec O M)). apply inversion_pole_vecteur; auto. auto with real. apply argument_affixe_produit_positif_vecteur_OM with (3 := H4); auto. apply aux_positif; auto. Qed.