proposition: Lemma inversion_pole_vecteur : forall (k : R) (O M M' : PO), k <> 0 -> O <> M -> M' = inversion O k M :>PO -> vec O M' = mult_PP (/ Rsqr (distance O M) * k) (vec O M) :>PP.
proof: Proof. intros. apply homothetie_vecteur. apply inversion_homothetie; auto. Qed.