proposition: Lemma orthogonaux_perce : forall A B C D E : PO, ~ alignes A B C -> D <> E -> orthogonaux (droite D E) (plan A B C) -> perce (droite D E) (plan A B C).
proof: Proof. intros. elim position_relative_droite_plan with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros H3; try clear position_relative_droite_plan; intros | intros H3; try clear position_relative_droite_plan; try exact H3 | auto | auto ]. absurd (D = E); auto. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros k H4; elim H4; intros k' H5; try clear H4; try exact H5 | auto | auto | auto ]. elim vecteurs_orthogonaux_rec with (A := A) (B := B) (C := C) (D := D) (E := E); [ try clear vecteurs_orthogonaux_rec; intros | auto | auto | auto ]. apply vecteur_nul_conf. apply scalaire_non_degenere. pattern (vec D E) at 1 in |- *; rewrite H5. cut (orthogonal (add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C))) (vec D E)); intros. elim existence_representant_comb_lin_vecteur with (A := A) (B := B) (C := A) (D := C) (a := k) (b := k'); intros E0 H8; try clear existence_representant_comb_lin_vecteur; rewrite <- H8. rewrite <- H8 in H6. rewrite (def_orthogonal (A:=A) (B:=E0) (C:=D) (D:=E)); auto. apply ortho_combinaison_lineaire; auto. Qed.