proposition: Lemma homothetie_inverse : forall (k : R) (I A A' : PO), k <> 0 :>R -> A' = homothetie k I A :>PO -> A = homothetie (/ k) I A' :>PO.
proof: Proof. intros. apply vecteur_homothetie. rewrite (homothetie_vecteur (k:=k) (I:=I) (A:=A) (A':=A')); auto. Fieldvec k. Qed.