proposition: Lemma vecteurs_orthogonaux_rec : forall A B C D E : PO, ~ alignes A B C -> D <> E -> orthogonaux (droite D E) (plan A B C) -> orthogonal (vec A B) (vec D E) /\ orthogonal (vec A C) (vec D E).
proof: Proof. intros. deroule_triangle A B C. elim def_orthogonaux2 with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros H5 H6; try clear def_orthogonaux2; try exact H6 | auto | auto | auto ]. intros. split; auto with geo. Qed.