proposition: Lemma translation_identite : forall I A A' : PO, A' = translation I I A :>PO -> A = A'.
proof: Proof. intros. apply vecteur_nul_conf; auto. rewrite <- (translation_vecteur (I:=I) (J:=I) (A:=A) (A':=A')); auto. Ringvec. Qed.