proposition: Lemma vec_normal_orthogonal_directeur : forall A B C D E F : PO, A <> B -> C <> D -> E <> F -> vec_normal (vec C D) (droite A B) -> orthogonal (vec C D) (vec E F) -> vec_directeur (vec E F) (droite A B).
proof: Proof. intros. apply paralleles_vec_directeur; auto. elim orthogonal_colineaires with (A := C) (B := D) (C := A) (D := B) (E := E) (F := F); [ 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.