proposition: Lemma vec_normal_paralleles_r : forall A B C D E F : PO, A <> B -> C <> D -> E <> F -> vec_normal (vec A B) (droite C D) -> vec_normal (vec A B) (droite E F) -> paralleles (droite C D) (droite E F).
proof: Proof. intros. elim orthogonal_colineaires with (A := A) (B := B) (C := E) (D := F) (E := C) (F := D); [ intros k H4; try clear orthogonal_colineaires; try exact H4 | auto | auto | auto with geo | auto with geo ]. apply colineaires_paralleles with k; auto. Qed.