proposition: Lemma translation_alignement : forall I J A A' B B' C C' : PO, A' = translation I J A :>PO -> B' = translation I J B :>PO -> C' = translation I J C -> alignes A B C -> alignes A' B' C'.
proof: Proof. intros I J A A' B 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 k. apply colineaire_alignes with k. rewrite <- (translation_bipoint (I:=I) (J:=J) (A:=A) (A':=A') (B:=B) (B':=B')) ; auto. rewrite <- H4; auto. rewrite <- (translation_bipoint (I:=I) (J:=J) (A:=A) (A':=A') (B:=C) (B':=C')) ; auto. Qed.