proposition: Lemma para_plan_sym : 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) -> para_plan_plan (plan D E F) (plan A B C).
proof: Proof. intros A B C D E F H H0 H1; try assumption. elim def_para_plan_plan2 with (A := A) (B := B) (C := C) (D := D) (E := E) (F := F); [ intros H2 H3; try clear def_para_plan_plan2; try exact H3 | auto | auto | auto ]. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := E); [ intros k H8; elim H8; intros k' H9; try clear H8 para_plan_dr_vecteur; auto | auto | auto | auto ]. elim para_plan_dr_vecteur with (A := A) (B := B) (C := C) (D := D) (E := F); [ intros k0 H10; elim H10; intros k'0 H11; try clear H10 para_plan_dr_vecteur; try exact H11 | auto | auto | auto ]. cut (ex (fun a : R => ex (fun b : R => vec A B = add_PP (mult_PP a (vec D E)) (mult_PP b (vec D F)))) /\ ex (fun c : R => ex (fun d : R => vec A C = add_PP (mult_PP c (vec D E)) (mult_PP d (vec D F))))). intros H12. elim H12; intros H13 H14; elim H13; intros a H15; elim H15; intros b H16; try clear H15 H13 H12; try exact H16. elim H14; intros c H12; elim H12; intros d H13; try clear H12 H14; try exact H13. apply couple_vecteurs_coplanaires with (a := a) (b := b) (c := c) (d := d); auto. cut (mult_PP k (vec D F) = add_PP (mult_PP (k * k0) (vec A B)) (mult_PP (k * k'0) (vec A C))); intros. cut (mult_PP k' (vec D F) = add_PP (mult_PP (k' * k0) (vec A B)) (mult_PP (k' * k'0) (vec A C))); intros. cut (mult_PP k0 (vec D E) = add_PP (mult_PP (k0 * k) (vec A B)) (mult_PP (k0 * k') (vec A C))); intros. cut (mult_PP k'0 (vec D E) = add_PP (mult_PP (k'0 * k) (vec A B)) (mult_PP (k'0 * k') (vec A C))); intros. cut (add_PP (mult_PP k (vec D F)) (mult_PP (- k0) (vec D E)) = mult_PP (k * k'0 + - (k0 * k')) (vec A C)); intros. cut (add_PP (mult_PP k' (vec D F)) (mult_PP (- k'0) (vec D E)) = mult_PP (k' * k0 + - (k'0 * k)) (vec A B)); intros. elim (classic (k * k'0 + - (k0 * k') = 0)); intros. cut (k' * k0 + - (k'0 * k) = 0); intros. rewrite H15 in H13. rewrite H14 in H12. elim (classic (k = 0)); intros. rewrite H16 in H15. rewrite H16 in H9. elim (classic (k' = 0)); intros. rewrite H17 in H9. absurd (D = E); auto with geo. apply conversion_PP with (a := 1) (b := 1); auto with *. unfold vec in H9. RingPP2 H9; RingPP. cut (k0 = 0); intros. clear H10; clear H8. rewrite H18 in H11. elim (classic (k'0 = 0)); intros. rewrite H8 in H11. absurd (D = F). apply non_alignes_distincts with E; auto. apply conversion_PP with (a := 1) (b := 1); auto with *. unfold vec in H11. RingPP2 H11; RingPP. absurd (alignes D E F); auto. apply colineaire_alignes with (k'0 * / k'); auto. rewrite H11; rewrite H9. unfold vec in |- *. FieldPP k'. cut (k' * k0 = 0); intros. RReplace k0 (/ k' * (k' * k0)). rewrite H18; field; auto. field; auto. rewrite <- H15; ring. absurd (alignes D E F); auto. apply colineaire_alignes with (/ k * k0); auto. cut (mult_PP k (vec D F) = mult_PP k0 (vec D E)); intros. apply mult_PP_regulier with k; auto. rewrite H17. FieldPP k. VReplace (mult_PP k0 (vec D E)) (add_PP (mult_PP k0 (vec D E)) (mult_PP 0 (vec A C))). rewrite <- H12; RingPP. RReplace (k' * k0 + - (k'0 * k)) (- (k * k'0 + - (k0 * k'))). rewrite H14; ring. cut (k' * k0 + - (k'0 * k) <> 0); intros. split; [ try assumption | idtac ]. exists (/ (k' * k0 + - (k'0 * k)) * - k'0); exists (/ (k' * k0 + - (k'0 * k)) * k'). apply mult_PP_regulier with (k' * k0 + - (k'0 * k)); auto. rewrite <- H13. FieldPP (k' * k0 + - (k'0 * k)). exists (/ (k * k'0 + - (k0 * k')) * - k0); exists (/ (k * k'0 + - (k0 * k')) * k). apply mult_PP_regulier with (k * k'0 + - (k0 * k')); auto with real. rewrite <- H12. FieldPP (k * k'0 + - (k0 * k')). RReplace (k' * k0 + - (k'0 * k)) (- (k * k'0 + - (k0 * k'))). auto with real. replace (mult_PP (- k'0) (vec D E)) with (add_PP (mult_PP (- k'0 * k) (vec A B)) (mult_PP (- k'0 * k') (vec A C))). rewrite H11; RingPP. apply mult_PP_regulier with (-1); auto with real. VReplace (mult_PP (-1) (mult_PP (- k'0) (vec D E))) (mult_PP k'0 (vec D E)). rewrite H7; RingPP. replace (mult_PP (- k0) (vec D E)) with (add_PP (mult_PP (- k0 * k) (vec A B)) (mult_PP (- k0 * k') (vec A C))). rewrite H4; RingPP. apply mult_PP_regulier with (-1); auto with real. VReplace (mult_PP (-1) (mult_PP (- k0) (vec D E))) (mult_PP k0 (vec D E)). rewrite H6; RingPP. rewrite H9; RingPP. rewrite H9; RingPP. rewrite H11; RingPP. rewrite H11; RingPP. apply non_alignes_distincts with E; auto. auto with geo. Qed.