proposition: Lemma image_translation_distincts : forall I J A A' B B' : PO, A <> B -> A' = translation I J A :>PO -> B' = translation I J B -> A' <> B'.
proof: Proof. intros. apply distinct_egalite_vecteur with (A := A) (B := B); auto. symmetry in |- *; apply translation_bipoint with (I := I) (J := J); auto. Qed.