proposition: Lemma inversion_est_homothetie : forall (I A B : PO) (k : R), k <> 0 -> I <> A -> (B = inversion I k A <-> B = homothetie (/ Rsqr (distance I A) * k) I A).
proof: Proof. intros; red in |- *; try split; intros. apply inversion_homothetie; auto. apply homothetie_inversion; auto. Qed.