proposition: Lemma argument_affixe_inversion_positif_conjugue : 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 (Cinv (Conj z)) :>AV.
proof: Proof. intros. assert (z <> zeroC). apply points_distincts_non_zeroC with (1 := H); auto with geo. assert (Conj z <> zeroC); auto with geo. rewrite (argument_affixe_inversion_pole_positif (k:=k) (M:=M) (M':=M') (z:=z) (z':=z')); auto. rewrite Cinv_argument; auto. rewrite argument_Conj2; auto. mes (argument z). RReplace (- - x) x; auto. Qed.