proposition: Theorem ecriture_complexe_inversion_pole_origine : forall (k : R) (z z' : C) (M M' : PO), O <> M -> k <> 0 -> z = affixe M -> z' = affixe M' -> (M' = inversion O k M <-> z' = Cmult (Rinj k) (Cinv (Conj z))).
proof: Proof. intros; red in |- *; try split; intros. apply (inversion_pole_origine_complexe (k:=k) (z:=z) (z':=z') (M:=M) (M':=M')); auto with geo. apply (complexe_inversion_pole_origine (k:=k) (z:=z) (z':=z') (M:=M) (M':=M')); auto with geo. Qed.