proposition: Lemma homothetie_neg : forall (I M M' : PO) (k : R), k < 0 -> M' = homothetie k I M -> M' = similitude I (- k) pi M.
proof: Proof. intros I M M' k H; try assumption. discrimine I M. rewrite <- homothetie_centre. rewrite <- similitude_def_centre; auto. lra. intros. cut (vec I M' = mult_PP k (vec I M)); intros. cut (distance I M' = Rabs k * distance I M); intros. 2: apply distance_homothetie with I; auto with geo. 2: apply homothetie_vecteur; auto. cut (I <> M'); intros. apply similitude_def2; auto. lra. rewrite <- Rabs_left; auto. rewrite (angle_produit_negatif_r (k:=k) (A:=I) (B:=M) (C:=M') (D:=I) (E:=M)); auto. rewrite <- angle_nul; auto. repeat rewrite <- add_mes_compatible. replace (0 + pi) with pi; auto. ring. apply distinct_produit_vecteur with (3 := H2); auto. auto with real. Qed.