proposition: Lemma plans_paralleles_droite : forall A B C D E F I J : PO, ~ alignes A B C -> ~ alignes D E F -> I <> J -> para_plan_plan (plan A B C) (plan D E F) -> para_plan_dr (plan A B C) (droite I J) -> para_plan_dr (plan D E F) (droite I J).
proof: Proof. intros. deroule_triangle A B C. deroule_triangle D E F. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := I) (E := J); [ intros k H10; elim H10; [ intros k' H11; try clear H10; try exact H11 ] | auto | auto | auto ]. elim plans_paralleles_vecteurs with (A := D) (B := E) (C := F) (D := A) (E := B) (F := C); auto. intros H10 H12; try assumption. elim H12; [ intros c H13; elim H13; [ intros d H14; try clear H13 H12; try exact H14 ] ]. elim H10; [ intros a H12; elim H12; [ intros b H13; try clear H12 H10; try exact H13 ] ]. cut (vec I J = add_PP (mult_PP k (add_PP (mult_PP a (vec D E)) (mult_PP b (vec D F)))) (mult_PP k' (add_PP (mult_PP c (vec D E)) (mult_PP d (vec D F))))); intros. apply vecteurs_para_plan_dr with (k := k * a + k' * c) (k' := k * b + k' * d); auto. rewrite H10; RingPP. rewrite H11; rewrite H14; rewrite H13; RingPP. apply para_plan_sym; auto. Qed.