proposition: Lemma image_homothetie_distincts : forall (k : R) (I A A' B B' : PO), k <> 0 :>R -> A <> B -> A' = homothetie k I A :>PO -> B' = homothetie k I B -> A' <> B'.
proof: Proof. intros. cut (vec A' B' <> zero); intros. red in |- *; intros; apply H3; auto. rewrite H4; Ringvec. rewrite (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B')); auto. red in |- *; intros. elim produit_vecteur_nul with (a := k) (A := A) (B := B); [ intros; try trivial | intros; try trivial | try trivial ]. absurd (k = 0); auto. absurd (A = B); auto. Qed.