proposition: Lemma existence_inversion : forall (I A : PO) (k : R), k <> 0 -> I <> A -> exists A' : PO, A' = inversion I k A.
proof: Proof. intros. elim existence_homothetique with (k := / Rsqr (distance I A) * k) (I := I) (A := A); [ intros A' H1; try clear existence_homothetique; try exact H1 ]. exists A'. apply homothetie_inversion; auto. Qed.