proposition: Theorem position_relative_droite_plan : forall A B C D E : PO, D <> E -> ~ alignes A B C -> para_plan_dr (plan A B C) (droite D E) \/ perce (droite D E) (plan A B C).
proof: Proof. unfold perce in |- *; intros. elim (classic (coplanaires A B C D)); intros. elim (classic (coplanaires A B C E)); intros. left; try assumption. apply paralleles_droite_incluse; auto. apply droite_incluse_plan2; auto. right; try assumption. split; [ idtac | try assumption ]. red in |- *; intros; apply H2. elim droite_incluse_plan with (A := A) (B := B) (C := C) (D := D) (E := E); [ try clear droite_incluse_plan; auto | auto | auto | auto ]. apply def_contact with D; auto with geo. lapply (points_plan_espace (A:=A) (B:=B) (C:=C) (D:=D) E); auto; intros. elim H2; [ intros H3; elim H3; [ intros k H4; elim H4; [ intros k' H5; try clear H4 H3 H2; try exact H5 ] ] | intros H3; try clear H2 ]. left; try assumption. apply vecteurs_para_plan_dr with (k := k) (k' := k'); auto. right; try assumption. elim H3; intros a H2; elim H2; intros b H4; elim H4; intros d H5; try clear H4 H2 H3; try exact H5. split; [ idtac | try assumption ]. red in |- *; intros; apply H1. elim droite_incluse_plan with (A := A) (B := B) (C := C) (D := D) (E := E); [ try clear droite_incluse_plan; auto | auto | auto | auto ]. apply def_contact with (barycentre (cons d D) (cons (1 + - d) E)); auto. apply barycentre_alignes; auto. replace (d + (1 + - d)) with 1. discrR. ring. unfold coplanaires, coplanaires1 in |- *. right; try assumption. pattern 1 at 1 in |- *. replace 1 with (d + (1 + - d)). rewrite <- add_PP_barycentre. rewrite H5. exists a; exists b; auto. replace (d + (1 + - d)) with 1. discrR. ring. ring. Qed.