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