proposition: Lemma translation_trans : forall I J A A' B B' : PO, A' = translation I J A :>PO -> B' = translation I J B :>PO -> B' = translation A A' B :>PO.
proof: Proof. intros I J A A' B B' H H0; try assumption. apply rec_translation_vecteur. rewrite <- (translation_vecteur (I:=I) (J:=J) (A:=A) (A':=A')); auto. rewrite <- (translation_vecteur (I:=I) (J:=J) (A:=B) (A':=B')); auto. Qed.