proposition: Lemma homothetie_alignement : forall (k : R) (I A B A' B' C C' : PO), A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> C' = homothetie k I C -> alignes A B C -> alignes A' B' C'.
proof: Proof. intros k I A B A' B' C C' H H0 H1 H2; try assumption. discrimine A B. assert (A' = B'); auto with geo. rewrite H0; rewrite <- H3; auto. halignes H2 k0. apply colineaire_alignes with k0. rewrite (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B')); auto. rewrite (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=C) (A':=A') (B':=C')); auto. rewrite H4. Ringvec. Qed.