proposition: Theorem inversion_positif_complexe : forall (k : R) (z z' : C) (M M' : PO), 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 -> z' = Cmult (Rinj k) (Cinv (Conj z)).
proof: Proof. intros. assert (k <> 0); auto with real. assert (z <> zeroC). apply points_distincts_non_zeroC with (1 := H); auto with geo. assert (Conj z <> zeroC); auto with geo. assert (O <> M'). apply image_distinct_pole with (3 := H3); auto with real. apply egalite_forme_polaire. apply points_distincts_non_zeroC with (1 := H7); auto with geo. apply nonzero_produit; auto with geo. rewrite (inversion_origine_module (k:=k) (z:=z) (z':=z') (M:=M) (M':=M')); auto. rewrite <- (module_Conj z). rewrite Cmult_module; auto. rewrite Cinv_module; auto. rewrite module_reel; auto. rewrite (argument_affixe_inversion_positif_conjugue (k:=k) (M:=M) (M':=M') (z:=z) (z':=z')); auto. rewrite Cmult_argument; auto with geo. rewrite argument_reel_pos; auto with real. mes (argument (Cinv (Conj z))). RReplace (0 + x) x; auto. Qed.