proposition: Lemma vecteurs_orthogonaux : forall A B C D E : PO, ~ alignes A B C -> D <> E -> orthogonal (vec A B) (vec D E) -> orthogonal (vec A C) (vec D E) -> orthogonaux (droite D E) (plan A B C).
proof: Proof. intros. deroule_triangle A B C. apply def_orthogonaux; auto with geo. Qed.