proposition: Lemma translation_inverse : forall I J A A' : PO, A' = translation I J A :>PO -> A = translation J I A' :>PO.
proof: Proof. intros. apply rec_translation_vecteur; auto. VReplace (vec J I) (mult_PP (-1) (vec I J)). rewrite (translation_vecteur (I:=I) (J:=J) (A:=A) (A':=A')); auto. Ringvec. Qed.