proposition: Lemma compo_transl : forall A A' A1 I J K L : PO, A1 = translation I J A -> A' = translation K L A1 -> vec A A' = add_PP (vec I J) (vec K L).
proof: Proof. intros A A' A1 I J K L H H0; try assumption. cut (vec K L = vec A1 A'); intros. cut (vec I J = vec A A1); intros. rewrite H1; rewrite H2; Ringvec. rewrite (translation_vecteur (I:=I) (J:=J) (A:=A) (A':=A1)); auto. apply translation_vecteur; auto. Qed.