proposition: Lemma vec_directeur_orthogonal_normal : forall A B C D E F : PO, A <> B -> C <> D -> E <> F -> vec_directeur (vec E F) (droite A B) -> orthogonal (vec C D) (vec E F) -> vec_normal (vec C D) (droite A B).
proof: Proof. intros. apply vec_normal_def2; auto. apply ortho_sym. elim determinant_nul_colinearite with (A := E) (B := F) (C := A) (D := B); [ intros k H4; try clear determinant_nul_colinearite; try exact H4 | auto | auto with geo ]. rewrite H4; auto with geo. Qed.