proposition: Lemma plans_paralleles_ou_droite_incluse2 : forall A B C D E F : PO, ~ alignes A B C -> ~ alignes D E F -> para_plan_plan (plan A B C) (plan D E F) \/ (exists I : PO, (exists J : PO, I <> J :>PO /\ incluse (droite I J) (plan A B C) /\ incluse (droite I J) (plan D E F))).
proof: Proof. intros A B C D E F H H0; try assumption. deroule_triangle D E F. elim position_relative_droite_plan with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros H4; try clear position_relative_droite_plan | intros H4; try clear position_relative_droite_plan; try exact H4 | try trivial | try trivial ]. elim position_relative_droite_plan with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros H5; try clear position_relative_droite_plan | intros H5; try clear position_relative_droite_plan; try exact H5 | try trivial | try trivial ]. left; try assumption. apply def_para_plan_plan; auto. elim H5; intros. elim def_contact2 with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros J H8; elim H8; [ intros H9 H10; try clear H8 def_contact2; try exact H10 ] | try trivial | try trivial | try trivial ]. right; try assumption. elim existence_representant_vecteur with (A := J) (B := E) (C := D); intros I; intros; try clear existence_representant_vecteur. exists I; exists J. cut (I <> J). intros H30. split; [ trivial | split; [ idtac | try assumption ] ]. cut (para_plan_dr (plan A B C) (droite J I)); intros. apply droite_incluse_plan2; auto. apply paralleles_droite_plan_coplanaires_incluse with (3 := H12); auto. apply paralleles_droites_plan_trans with (4 := H4); auto. apply def_paralleles with (-1); auto. unfold vec in H11. VReplace (cons (-1) I) (mult_PP (-1) (cons 1 I)). RingPP2 H11. Ringvec. cut (coplanaires D E F J). intros H20. apply droite_incluse_plan2; auto. cut (para_plan_dr (plan D E F) (droite J I)); intros. apply paralleles_droite_plan_coplanaires_incluse with (3 := H12); auto. apply def_para_plan_dr with (D := D) (E := E); auto with geo. apply def_paralleles with (-1); auto. unfold vec in H11. VReplace (cons (-1) I) (mult_PP (-1) (cons 1 I)). RingPP2 H11. Ringvec. unfold coplanaires in |- *. hPPalignes H9 k. right; try assumption. exists k; exists 0. rewrite H9; RingPP. unfold vec in H11. unfold not in |- *; intros; apply H3. apply conversion_PP with (a := 1) (b := 1); auto. cut (add_PP (cons (-1) E) (cons 1 D) = add_PP (cons (-1) J) (cons 1 I)); intros; auto. RingPP2 H13. rewrite H12; RingPP. auto with *. elim position_relative_droite_plan with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros H5; try clear position_relative_droite_plan | unfold perce in |- *; intros H5; try clear position_relative_droite_plan; try exact H5 | try trivial | try trivial ]. elim def_contact2 with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros J H6; elim H6; [ intros H7 H8; try clear H6 def_contact2; try exact H8 ] | try trivial | try trivial | try trivial ]. right; try assumption. elim existence_representant_vecteur with (A := J) (B := D) (C := F); intros I; intros; try clear existence_representant_vecteur; try exact H5. exists I; exists J. cut (I <> J). intros H30. split; [ trivial | split; [ idtac | try assumption ] ]. cut (para_plan_dr (plan A B C) (droite J I)); intros. apply droite_incluse_plan2; auto. apply paralleles_droite_plan_coplanaires_incluse with (3 := H10); auto. apply paralleles_droites_plan_trans with (4 := H5); auto. apply def_paralleles with 1; auto. unfold vec in H9; auto. RingPP2 H9. RingPP. cut (coplanaires D E F J); auto with geo. intros H20. apply droite_incluse_plan2; auto. cut (para_plan_dr (plan D E F) (droite J I)); intros. apply paralleles_droite_plan_coplanaires_incluse with (3 := H10); auto with geo. apply def_para_plan_dr with (D := D) (E := F); auto with geo. apply def_paralleles with 1; auto. unfold vec in H9. RingPP2 H9. RingPP. unfold vec in H9. unfold not in |- *; intros; apply H1. apply conversion_PP with (a := 1) (b := 1); auto. cut (add_PP (cons (-1) F) (cons 1 D) = add_PP (cons 1 J) (cons (-1) I)); intros; auto. RingPP2 H11. rewrite H10; RingPP. VReplace (cons (-1) I) (mult_PP (-1) (cons 1 I)). RingPP2 H9. RingPP. auto with *. unfold perce in H4. elim H4; [ intros H6 H7; try clear H4; try exact H7 ]. elim def_contact2 with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros J H6; elim H6; [ intros H7 H8; try clear H6; try exact H8 ] | trivial | trivial | trivial ]. elim def_contact2 with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros I H6; elim H6; [ intros H9 H10; try clear H6; try exact H10 ] | trivial | trivial | trivial ]. right. elim (classic (I = J)); intros. cut (I = D); intros. elim position_relative_droite_plan with (A := A) (B := B) (C := C) (D := E) (E := F); [ intros H12; try clear position_relative_droite_plan | unfold perce in |- *; intros H12; try clear position_relative_droite_plan; trivial | trivial | trivial ]. elim existence_representant_vecteur with (A := I) (B := E) (C := F); intros K H13; try clear existence_representant_vecteur. cut (E <> F); intros. cut (I <> K); intros. exists I; exists K. split; [ trivial | split; [ idtac | try assumption ] ]. apply droite_incluse_plan2; auto with geo. cut (para_plan_dr (plan A B C) (droite I K)); intros. apply paralleles_droite_plan_coplanaires_incluse with (3 := H16); auto with geo. apply paralleles_droites_plan_trans with (4 := H12); auto with geo. apply def_paralleles with 1; auto. unfold vec in H13. RingPP2 H13. RingPP. apply droite_incluse_plan2; auto with geo. apply paralleles_droite_plan_coplanaires_incluse with (D := I) (E := K); auto with geo. apply def_para_plan_dr with (D := E) (E := F); auto with geo. apply def_paralleles with 1; auto. unfold vec in H13. RingPP2 H13. RingPP. unfold not in |- *; intros; apply H14. apply conversion_PP with (a := 1) (b := 1); auto. unfold vec in H12. cut (add_PP (cons (-1) E) (cons 1 F) = add_PP (cons (-1) I) (cons 1 K)); intros; auto. RingPP2 H16. rewrite H15; RingPP. auto with *. elim H12; [ intros H13 H14; try clear H12; try exact H14 ]. elim def_contact2 with (A := A) (B := B) (C := C) (D := E) (E := F); [ intros K H12; try clear def_perce2; try exact H8 | trivial | trivial | trivial ]. elim H12; [ intros H15 H16; try clear H12; try exact H16 ]. exists I; exists K. cut (I <> K); intros. split; [ trivial | split; [ idtac | try assumption ] ]. apply droite_incluse_plan2; auto. apply droite_incluse_plan2; auto. rewrite H11; auto with geo. auto with geo. rewrite H11; auto. unfold not in |- *; intros; apply H0. rewrite H12; auto with geo. apply concours_unique with (A := D) (A1 := E) (B := F) (B1 := D); auto with geo. rewrite H6; auto. exists I; exists J. split; [ trivial | split; [ idtac | try assumption ] ]. apply droite_incluse_plan2; auto. apply droite_incluse_plan2; auto. auto with geo. auto with geo. elim H5; [ intros H6 H9; try clear H5; try exact H9 ]. elim H4; auto. Qed.