proposition: Lemma plans_paralleles_vecteurs : 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 a : R, (exists b : R, vec D E = add_PP (mult_PP a (vec A B)) (mult_PP b (vec A C)) :>PP)) /\ (exists c : R, (exists d : R, vec D F = add_PP (mult_PP c (vec A B)) (mult_PP d (vec A C)) :>PP)).
proof: Proof. intros. elim def_para_plan_plan2 with (3 := H1); [ try clear def_para_plan_plan2; auto | auto | auto ]. intros. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros k H5; elim H5; intros k' H6; try clear H5 para_plan_dr_vecteur; try exact H6 | auto with geo | auto | auto ]. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros k0 H7; elim H7; intros k'0 H8; try clear H7 para_plan_dr_vecteur; try exact H8 | auto with geo | auto | auto ]. split; [ exists k | idtac ]. exists k'; auto. exists k0; exists k'0; auto. deroule_triangle D E F; auto. Qed.