proposition: Lemma para_plan_trans : forall A B C D E F G H I : PO, ~ alignes A B C -> ~ alignes D E F -> ~ alignes G H I -> para_plan_plan (plan A B C) (plan D E F) -> para_plan_plan (plan D E F) (plan G H I) -> para_plan_plan (plan A B C) (plan G H I).
proof: Proof. intros A B C D E F G H I H0 H1 H2 H3 H4; try assumption. deroule_triangle A B C. deroule_triangle D E F. deroule_triangle G H I. elim def_para_plan_plan2 with (A := A) (B := B) (C := C) (D := D) (E := E) (F := F); [ intros H14 H15; try clear def_para_plan_plan2; auto | auto | auto | auto ]. elim def_para_plan_plan2 with (A := D) (B := E) (C := F) (D := G) (E := H) (F := I); [ intros; auto | auto | auto | auto ]. elim def_para_plan_plan2 with (A := D) (B := E) (C := F) (D := G) (E := H) (F := I); [ try clear def_para_plan_plan2; auto | auto | auto | auto ]. intros. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros k H20; elim H20; [ intros k' H21; try clear H20; auto ] | auto | auto | auto ]. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros k0 H22; elim H22; [ intros k'0 H23; try clear H22; auto ] | auto | auto | auto ]. elim para_plan_dr_vecteur with (A := D) (B := E) (C := F) (D := G) (E := H); [ intros k1 H20; elim H20; [ intros k'1 H22; try clear H20; auto ] | auto | auto | auto ]. elim para_plan_dr_vecteur with (A := D) (B := E) (C := F) (D := G) (E := I); [ intros k2 H20; elim H20; [ intros k'2 H24; try clear H20; auto ] | auto | auto | auto ]. cut (ex (fun a : R => ex (fun b : R => vec G I = add_PP (mult_PP a (vec A B)) (mult_PP b (vec A C)))) /\ ex (fun c : R => ex (fun d : R => vec G H = add_PP (mult_PP c (vec A B)) (mult_PP d (vec A C))))); intros. elim H20; [ intros H25 H26; elim H25; [ intros a H27; elim H27; [ intros b H28; try clear H27 H25 H20; try exact H28 ] ] ]. elim H26; [ intros c H20; elim H20; [ intros d H25; try clear H20 H26; try exact H25 ] ]. apply couple_vecteurs_coplanaires with (a := c) (b := d) (c := a) (d := b); auto. split; [ try assumption | idtac ]. cut (vec G I = add_PP (mult_PP k2 (add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)))) (mult_PP k'2 (add_PP (mult_PP k0 (vec A B)) (mult_PP k'0 (vec A C))))); intros. exists (k2 * k + k'2 * k0). exists (k2 * k' + k'2 * k'0). rewrite H20; RingPP. rewrite <- H21; rewrite <- H23; rewrite H24; auto. cut (vec G H = add_PP (mult_PP k1 (add_PP (mult_PP k (vec A B)) (mult_PP k' (vec A C)))) (mult_PP k'1 (add_PP (mult_PP k0 (vec A B)) (mult_PP k'0 (vec A C))))); intros. exists (k1 * k + k'1 * k0). exists (k1 * k' + k'1 * k'0). rewrite H20; RingPP. rewrite <- H21; rewrite <- H23; rewrite H22; auto. Qed.