proposition: Lemma plans_paralleles_secants_droites_paralleles : forall A B C D E F I J K : PO, ~ alignes A B C -> ~ alignes D E F -> ~ alignes I J K -> para_plan_plan (plan A B C) (plan D E F) -> ~ para_plan_plan (plan A B C) (plan I J K) -> incluse (droite I J) (plan A B C) -> ex (fun G : PO => ex (fun L : PO => (G <> L /\ incluse (droite G L) (plan I J K)) /\ incluse (droite G L) (plan D E F) /\ paralleles (droite G L) (droite I J))).
proof: Proof. intros. deroule_triangle A B C. deroule_triangle D E F. deroule_triangle I J K. cut (para_plan_dr (plan D E F) (droite I J)); intros. elim position_relative_droite_plan with (A := D) (B := E) (C := F) (D := I) (E := K); [ intros H15; try clear position_relative_droite_plan | unfold perce in |- *; intros H15; try clear position_relative_droite_plan; try exact H15 | try trivial | try trivial ]. 2: elim H15; [ intros H16 H17; try clear H15; try exact H17 ]. cut (para_plan_plan (plan D E F) (plan I J K)); intros. absurd (para_plan_plan (plan A B C) (plan I J K)); auto. apply para_plan_trans with (D := D) (E := E) (F := F); auto. apply def_para_plan_plan; auto. elim def_contact2 with (3 := H17); [ intros G H15; elim H15; intros; try clear H15; auto | auto | auto ]. elim existence_representant_vecteur with (A := G) (B := I) (C := J); intros L H20; try clear existence_representant_vecteur. exists G; exists L. cut (G <> L); intros. cut (paralleles (droite G L) (droite I J)); intros. split; [ split; [ try assumption | idtac ] | idtac ]. cut (coplanaires I J K G); intros. apply droite_incluse_plan2; auto with geo. apply paralleles_droite_plan_coplanaires_incluse with (D := G) (E := L); auto. apply vecteurs_para_plan_dr with (k := 1) (k' := 0); auto. rewrite H20; RingPP. auto with geo. split; [ try assumption | auto ]. cut (para_plan_dr (plan D E F) (droite G L)); intros. apply droite_incluse_plan2; auto with geo. apply paralleles_droite_plan_coplanaires_incluse with (D := G) (E := L); auto. apply paralleles_droites_plan_trans with (D := I) (E := J); auto with geo. apply colineaires_paralleles with 1; auto with geo. rewrite H20; RingPP. unfold not in |- *; intros; apply H13. apply conversion_PP with (a := 1) (b := 1); auto with *. cut (vec I J = vec G L); intros. unfold vec in H21. RingPP2 H21. rewrite H15; RingPP. rewrite H20; auto. apply plans_paralleles_droite with (4 := H2); auto. apply paralleles_droite_incluse; auto. Qed.