proposition: Lemma translation_paralleles : forall I J A A' B B' C C' D D' : PO, A <> B -> C <> D -> paralleles (droite A B) (droite C D) -> A' = translation I J A :>PO -> B' = translation I J B -> C' = translation I J C :>PO -> D' = translation I J D :>PO -> paralleles (droite A' B') (droite C' D').
proof: Proof. intros. elim paralleles_vecteur with (A := A) (B := B) (C := C) (D := D); [ intros k H6; try clear paralleles_vecteur; try exact H6 | auto | auto | auto ]. apply colineaires_paralleles with k. apply distinct_egalite_vecteur with (A := A) (B := B); auto. symmetry in |- *; apply translation_bipoint with (I := I) (J := J); auto. apply distinct_egalite_vecteur with (A := C) (B := D); auto. symmetry in |- *; apply translation_bipoint with (I := I) (J := J); auto. rewrite <- (translation_bipoint (I:=I) (J:=J) (A:=C) (A':=C') (B:=D) (B':=D')) ; auto. rewrite <- H6; auto. symmetry in |- *; apply translation_bipoint with (I := I) (J := J); auto. Qed.