proposition: Lemma translation_droite : forall I J A A' B B' : PO, A <> B -> A' = translation I J A :>PO -> B' = translation I J B :>PO -> paralleles (droite A' B') (droite A B).
proof: Proof. intros. apply colineaires_paralleles with 1; auto. apply image_translation_distincts with (2 := H0) (3 := H1); auto. replace (mult_PP 1 (vec A B)) with (vec A B). symmetry in |- *; apply translation_bipoint with (I := I) (J := J); auto. Ringvec. Qed.