proposition: Lemma translation_vecteur : forall I J A A' : PO, A' = translation I J A -> vec I J = vec A A'.
proof: Proof. unfold vec, translation in |- *; intros. rewrite H. pattern 1 at 2 in |- *. replace 1 with (-1 + 2); try ring. rewrite <- add_PP_barycentre; try discrR. replace 2 with (1 + 1) by ring. rewrite <- add_PP_barycentre; try discrR. RingPP. Qed.