proposition: Lemma homothetie_neg2 : forall (I M : PO) (k : R), k < 0 -> homothetie k I M = similitude I (- k) pi M.
proof: Proof. intros. elim existence_homothetique with (k := k) (I := I) (A := M); intros M'; intros. rewrite <- H0. apply homothetie_neg; auto. Qed.