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