proposition: Theorem position_relative_plans_paralleles : 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) -> disjoints (plan A B C) (plan D E F) \/ confondus (plan A B C) (plan D E F).
proof: Proof. intros A B C D E F H H0 H3; try assumption. intros. assert (A <> B); auto with geo. assert (D <> E); auto with geo. elim (classic (disjoints (plan A B C) (plan D E F))); intros. left; try assumption. right; try assumption. elim non_disjoints_exists with (3 := H4); [ intros I H5; try clear non_disjoints_exists; try exact H3 | auto | auto ]. elim H5; [ intros H6 H7; try clear H5; try exact H6 ]. apply def_confondus; auto. intros J H5; try assumption. elim plans_paralleles_vecteurs with (A := D) (B := E) (C := F) (D := A) (E := B) (F := C); auto. intros. elim H9; intros c H10; elim H10; intros d H11; try clear H10 H9; try exact H11. elim H8; intros a H9; elim H9; intros b H10; try clear H9 H8; try exact H10. hcoplanaires H5 x k'. hcoplanaires H6 x0 k'0. hcoplanaires H7 x1 k'1. apply (vecteur_def_coplanaires (k:=x1 + -1 * (x0 * a + k'0 * c) + (x * a + k' * c)) (k':=k'1 + -1 * (x0 * b + k'0 * d) + (x * b + k' * d))). replace (vec D J) with (add_PP (add_PP (vec D I) (mult_PP (-1) (vec A I))) (vec A J)). rewrite H7. rewrite H6. rewrite H5. rewrite H10. rewrite H11. Ringvec. Ringvec. apply para_plan_sym; auto. Qed.