proposition: Lemma composition_translation : forall A A' A1 I J K L : PO, A1 = translation I J A -> A' = translation K L A1 -> ex (fun M : PO => vec I M = add_PP (vec I J) (vec K L) :>PP /\ A' = translation I M A).
proof: Proof. intros A A' A1 I J K L H H0; try assumption. elim existence_representant_som_vecteur with (A := I) (B := J) (C := K) (D := L); intros M H1; try clear existence_representant_som_vecteur; try exact H1. exists M. split; [ try assumption | idtac ]. apply rec_translation_vecteur. rewrite H1. symmetry in |- *; apply compo_transl with A1; auto. Qed.