proposition: Theorem toit : forall A B C D E F : PO, ~ alignes A B C -> ~ alignes D E F -> paralleles (droite D E) (droite A B) -> ~ para_plan_plan (plan A B C) (plan D E F) -> exists I : PO, (exists J : PO, (I <> J :>PO /\ paralleles (droite A B) (droite I J)) /\ incluse (droite I J) (plan A B C) /\ incluse (droite I J) (plan D E F)).
proof: Proof. intros. deroule_triangle A B C. deroule_triangle D E F. elim position_relative_droite_plan with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros H9; try clear position_relative_droite_plan | unfold perce in |- *; intros H9; try clear position_relative_droite_plan; try exact H9 | try trivial | trivial ]. 2: elim H9; [ intros H10 H11; try clear H9; try exact H11 ]. absurd (para_plan_plan (plan A B C) (plan D E F)); auto. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros k H10; elim H10; [ intros k' H11; try clear H10 para_plan_dr_vecteur; auto ] | auto | auto | auto ]. elim paralleles_vecteur with (A := D) (B := E) (C := A) (D := B); [ intros k0 H12; try clear paralleles_vecteur; auto | auto | auto | auto ]. apply couple_vecteurs_coplanaires with (a := k0) (b := 0) (c := k) (d := k'); auto. rewrite H12; RingPP. elim def_contact2 with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros I H12; try clear def_secants2 | trivial | trivial | trivial ]. elim H12; [ intros H9 H13; try clear H12; try exact H13 ]. exists I. elim existence_representant_vecteur with (A := I) (B := A) (C := B); intros J H14; try clear existence_representant_vecteur. exists J. cut (I <> J). intros H21. cut (paralleles (droite A B) (droite I J)). intros H16; try assumption. split; [ split; [ try assumption | idtac ] | idtac ]. try exact H16. split; [ try assumption | idtac ]. apply droite_incluse_plan2; auto. apply paralleles_droite_plan_coplanaires_incluse with (D := I) (E := J); auto. apply def_para_plan_dr with (D := A) (E := B); auto with geo. cut (coplanaires D E F I). intros H22. apply droite_incluse_plan2; auto. cut (paralleles (droite D E) (droite I J)); intros. apply paralleles_droite_plan_coplanaires_incluse with (D := I) (E := J); auto. apply def_para_plan_dr with (D := D) (E := E); auto with geo. apply paralleles_trans with (5 := H16); auto. auto with geo. apply colineaires_paralleles with 1; auto. rewrite H14; RingPP. unfold not in |- *; intros; apply H5. apply conversion_PP with (a := 1) (b := 1); auto with *. cut (vec A B = vec I J); intros. unfold vec in H15. RingPP2 H15. rewrite H12; RingPP. rewrite H14; auto. Qed.