proposition: Lemma homothetie_inversion : forall (I A B : PO) (k : R), k <> 0 -> I <> A -> B = homothetie (/ Rsqr (distance I A) * k) I A -> B = inversion I k A.
proof: Proof. intros. generalize (homothetie_vecteur H1); intros. apply inversion_def2; auto. apply colineaire_alignes with (/ Rsqr (distance I A) * k); auto. rewrite H2; Simplscal. unfold Rsqr in |- *; rewrite <- carre_scalaire_distance. field; auto with geo. Qed.