proposition: Lemma perpendiculaires_orthogonales : forall A B C D : PO, A <> B -> C <> D -> perpendiculaires (droite A B) (droite C D) -> orthogonales (droite A B) (droite C D).
proof: Proof. intros. elim def_perpendiculaires2 with (A := A) (B := B) (C := C) (D := D); [ intros; try exact H3 | auto | auto | auto ]. Qed.