proposition: Lemma inversion_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. deroule_inversion I A B k. apply vecteur_homothetie. halignes H2 k0. assert (k0 = / Rsqr (distance I A) * k). apply Rmult_eq_reg_l with (scalaire (vec I A) (vec I A)); auto with geo. replace (scalaire (vec I A) (vec I A) * k0) with (scalaire (vec I A) (vec I B)). unfold Rsqr in |- *; rewrite <- carre_scalaire_distance. rewrite <- H3. field; auto with geo. rewrite H5; Simplscal. rewrite H5; rewrite H6; auto. Qed.