Require Export GeoCoq.Tarski_dev.Ch14_prod.

Section Order.

Context `{T2D:Tarski_2D}.
Context `{TE:@Tarski_euclidean Tn TnEQD}.

Lemma l14_36_a : forall O E E' A B C,
 Sum O E E' A B C -> Out O A B -> Bet O A C.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    assert(HS:=H).
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    unfold Sum in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ar2 Tn O E E' A B A *)
    unfold Ar2 in H.
(* Goal: False *)
    unfold Out in H0.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Bet Tn O A C *)
    assert(Parallelogram_flat O A C B).
(* Goal: @Parallelogram_flat Tn O A C B *)
(* Goal: @Bet Tn O A C *)
      apply(sum_cong O E E' H A B C HS).
(* Goal: @eq (@Tpoint Tn) A A *)
      tauto.
(* Goal: @Bet Tn O A C *)
    assert(Parallelogram O A C B).
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      right.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @Bet Tn O A C *)
    induction(eq_dec_points A B).
(* Goal: or (@LtP Tn O E E' A B) (@eq (@Tpoint Tn) A B) *)
      subst B.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      unfold Parallelogram_flat in H7.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      spliter.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      assert(O = C \/ Midpoint A O C).
(* Goal: or (@eq (@Tpoint Tn) O C) (@Midpoint Tn A O C) *)
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
        apply(l7_20 A O C).
(* Goal: @Col Tn O E E' *)
(* Goal: @Ps Tn O E AB *)
          ColR.
(* Goal: @Cong Tn O A O MA *)
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
        Cong.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      induction H13.
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
        subst C.
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
        apply False_ind.
(* Goal: False *)
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
        apply HS.
(* Goal: @eq (@Tpoint Tn) A B *)
        apply (double_null_null O E E') in HS; auto.
(* Goal: @eq (@Tpoint Tn) A A *)
        tauto.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      unfold Midpoint in H13.
(* Goal: @eq (@Tpoint Tn) A A *)
      tauto.
(* Goal: @Bet Tn O A C *)
    induction H3.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      apply plg_permut in H8.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      apply plg_permut in H8.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      apply plg_permut in H8.
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
      assert(Bet A B C).
(* Goal: @Bet Tn mA O E *)
        apply between_symmetry.
(* Goal: @Bet Tn C B A *)
(* Goal: @Bet Tn O A C *)
(* Goal: @Bet Tn O A C *)
        apply(plg_bet1 B O A C).
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
          assumption.
(* Goal: @Bet Tn mA O E *)
        apply between_symmetry.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
        assumption.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply (outer_transitivity_between O A B C); auto.
(* Goal: @Bet Tn O A C *)
    assert(Bet B A C).
(* Goal: @Bet Tn mA O E *)
      apply between_symmetry.
(* Goal: @Bet Tn C A B *)
(* Goal: @Bet Tn O A C *)
      apply(plg_bet1 A O B C).
(* Goal: @Parallelogram Tn A O B C *)
(* Goal: @Bet Tn A B O *)
(* Goal: @Bet Tn O A C *)
        apply plg_comm2.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
        assumption.
(* Goal: @Bet Tn mA O E *)
      apply between_symmetry.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assumption.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply (outer_transitivity_between2 O B A C); auto.
Qed.

Lemma l14_36_b : forall O E E' A B C,
 Sum O E E' A B C -> Out O A B -> O <> A /\ O <> C /\ A <> C.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: and (not (@eq (@Tpoint Tn) O A)) (and (not (@eq (@Tpoint Tn) O C)) (not (@eq (@Tpoint Tn) A C))) *)
    assert(HH:= l14_36_a O E E' A B C H H0).
(* Goal: False *)
    unfold Out in H0.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @eq (@Tpoint Tn) A B *)
    split; auto.
(* Goal: and (@Diff Tn O E E' C A dCA) (@Ps Tn O E dCA) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
    split.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      subst C.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
      apply between_identity in HH.
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
      subst A.
(* Goal: @eq (@Tpoint Tn) A A *)
      tauto.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
    intro.
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
    subst C.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    assert(HS:= H).
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    unfold Sum in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ar2 Tn O E E' A B A *)
    unfold Ar2 in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: False *)
    assert(Sum O E E' A O A).
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      apply (sum_A_O). assumption.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    assumption.
(* Goal: False *)
    assert(B = O).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply (sum_uniquenessB O E E' H A B O A); auto.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      contradiction.
Qed.

(** Lemma 14.37 *)
Lemma O_not_positive : forall O E, ~ Ps O E O.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ps Tn O E MA *)
    unfold Ps.
(* Goal: @Out Tn O E MA *)
    unfold Out.
(* Goal: not (and (not (@eq (@Tpoint Tn) O O)) (and (not (@eq (@Tpoint Tn) E O)) (or (@Bet Tn O O E) (@Bet Tn O E O)))) *)
    intuition.
Qed.

Lemma pos_null_neg : forall O E E' A MA,
 Opp O E E' A MA -> Ps O E A \/ O = A \/ Ps O E MA.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    unfold Opp in H.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    induction (eq_dec_points A O).
(* Goal: @eq (@Tpoint Tn) A B *)
      right; left; auto.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    assert(HS:= H).
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    unfold Sum in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ar2 Tn O E E' A B A *)
    unfold Ar2 in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    assert(Parallelogram_flat O MA O A).
(* Goal: @eq (@Tpoint Tn) A A *)
      apply(sum_cong O E E' H MA A O HS); tauto.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    unfold Parallelogram_flat in H5.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    assert(HG:=grid_not_par O E E' H).
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    assert(A = MA \/ Midpoint O A MA).
(* Goal: @Col Tn O E E' *)
(* Goal: @Ps Tn O E AB *)
      apply(l7_20 O A MA); try ColR.
(* Goal: @Cong Tn O A O MA *)
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
      Cong.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    induction H16.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      subst MA.
(* Goal: @eq (@Tpoint Tn) A A *)
      tauto.
(* Goal: or (@Ps Tn O E A) (or (@eq (@Tpoint Tn) O A) (@Ps Tn O E MA)) *)
    induction(out_dec O E A).
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left.
(* Goal: @Ps Tn O E MA *)
      unfold Ps.
(* Goal: @Out Tn O MA E *)
      apply l6_6.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assumption.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    right; right.
(* Goal: @Ps Tn O E MA *)
    assert(MA <> O).
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      subst MA.
(* Goal: False *)
(* Goal: @Ps Tn O E MA *)
      apply is_midpoint_id_2 in H16.
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
      subst A.
(* Goal: @eq (@Tpoint Tn) A A *)
      tauto.
(* Goal: @Ps Tn O E MA *)
    unfold Midpoint in H16.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ps Tn O E MA *)
    unfold Ps.
(* Goal: @Out Tn O MA E *)
    unfold Col in H2.
(* Goal: False *)
    induction H2.
(* Goal: @Out Tn O E MA *)
      unfold Out.
(* Goal: @eq (@Tpoint Tn) A B *)
      repeat split; auto.
(* Goal: False *)
    induction H2.
(* Goal: @Out Tn O E MA *)
      unfold Out.
(* Goal: and (not (@eq (@Tpoint Tn) E' A)) (and (not (@eq (@Tpoint Tn) E' A)) (and (@Col Tn E' E' A) (@Col Tn A E' A))) *)
(* Goal: @Ps Tn O E AB *)
      repeat split; Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left.
(* Goal: @Bet Tn mA O E *)
      apply between_symmetry.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
    apply False_ind.
(* Goal: False *)
    apply H17.
(* Goal: @Out Tn O E MA *)
    unfold Out.
(* Goal: @eq (@Tpoint Tn) A B *)
    repeat split; auto.
(* Goal: or (@Bet Tn O E A) (@Bet Tn O A E) *)
    apply between_symmetry in H16.
(* Goal: or (@Bet Tn O E A) (@Bet Tn O A E) *)
    assert(HH:= l5_2 MA O A E H18 H16 H2).
(* Goal: @eq (@Tpoint Tn) A A *)
    tauto.
Qed.

Lemma sum_pos_pos : forall O E E' A B AB,
  Ps O E A -> Ps O E B -> Sum O E E' A B AB -> Ps O E AB.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ps Tn O E AB *)
    unfold Ps in *.
(* Goal: @Out Tn O AB E *)
    assert(Out O A B).
(* Goal: @Out Tn O A B *)
(* Goal: @Out Tn O AB E *)
      apply l6_6 in H0.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply(l6_7 O A E B); auto.
(* Goal: @Out Tn O AB E *)
    assert(HH:=l14_36_b O E E' A B AB H1 H2).
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Out Tn O AB E *)
    assert(HH:=l14_36_a O E E' A B AB H1 H2).
(* Goal: @Out Tn O AB E *)
    apply l6_6 in H.
(* Goal: @Out Tn O AB E *)
    assert(Out O A AB).
(* Goal: @eq (@Tpoint Tn) A B *)
      apply bet_out; auto.
(* Goal: @Out Tn O AB E *)
    assert(HP:=l6_7 O E A AB H H6).
(* Goal: @Out Tn O MA E *)
    apply l6_6.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    assumption.
Qed.

Lemma prod_pos_pos : forall O E E' A B AB,
 Ps O E A -> Ps O E B -> Prod O E E' A B AB -> Ps O E AB.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ps Tn O E AB *)
    assert(HP:= H1).
(* Goal: @Ps Tn O E AB *)
    unfold Prod in H1.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ng Tn O E mA *)
    unfold Ar2 in H1.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ps Tn O E AB *)
    ex_and H2 B'.
(* Goal: @Ps Tn O E AB *)
    assert(HG:= grid_not_par O E E' H1).
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: False *)
    unfold Ps in H.
(* Goal: False *)
    unfold Ps in H0.
(* Goal: @Ps Tn O E AB *)
    unfold Out in *.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ps Tn O E AB *)
    assert(E' <> A).
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
      subst A.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      contradiction.
(* Goal: @Ps Tn O E AB *)
    assert(~Col O E' A).
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
      apply H1.
(* Goal: @Col Tn O E E' *)
(* Goal: @Ps Tn O E AB *)
      ColR.
(* Goal: @Ps Tn O E AB *)
    assert(~Par O E E' A).
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
      induction H20.
(* Goal: False *)
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
        apply H20.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X O E) (@Col Tn X E' A)) *)
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
        exists A.
(* Goal: and (@Col Tn A O E) (@Col Tn A E' A) *)
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
        split; Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      spliter.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      contradiction.
(* Goal: @Ps Tn O E AB *)
    assert(Proj E E' O E' E E').
(* Goal: @Proj Tn O O O E E' A *)
(* Goal: @Ps Tn O E AB *)
      apply(pj_col_project); Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left; right.
(* Goal: and (not (@eq (@Tpoint Tn) E' A)) (and (not (@eq (@Tpoint Tn) E' A)) (and (@Col Tn E' E' A) (@Col Tn A E' A))) *)
(* Goal: @Ps Tn O E AB *)
      repeat split; Col.
(* Goal: @Ps Tn O E AB *)
    assert(Proj B B' O E' E E').
(* Goal: @Proj Tn O O O E E' A *)
(* Goal: @Ps Tn O E AB *)
      apply(pj_col_project); Col.
(* Goal: @Ps Tn O E AB *)
    assert(Proj O O O E' E E').
(* Goal: @Proj Tn O O O E E' A *)
(* Goal: @Ps Tn O E AB *)
      apply(pj_col_project); Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      right.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @Ps Tn O E AB *)
    assert(Proj E' A O E E' A).
(* Goal: @Proj Tn O O O E E' A *)
(* Goal: @Ps Tn O E AB *)
      apply(pj_col_project); Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left; right.
(* Goal: and (not (@eq (@Tpoint Tn) E' A)) (and (not (@eq (@Tpoint Tn) E' A)) (and (@Col Tn E' E' A) (@Col Tn A E' A))) *)
(* Goal: @Ps Tn O E AB *)
      repeat split; Col.
(* Goal: @Ps Tn O E AB *)
    assert(Proj B' AB O E E' A).
(* Goal: @Proj Tn O O O E E' A *)
(* Goal: @Ps Tn O E AB *)
      apply(pj_col_project); Col.
(* Goal: @Ps Tn O E AB *)
    assert(Proj O O O E E' A).
(* Goal: @Proj Tn O O O E E' A *)
(* Goal: @Ps Tn O E AB *)
      apply(pj_col_project); Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      right.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @Ps Tn O E AB *)
    assert(AB <> O).
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
      subst AB.
(* Goal: False *)
(* Goal: @Ps Tn O E AB *)
      apply prod_null in HP.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      induction HP; contradiction.
(* Goal: @Ps Tn O E MA *)
    unfold Ps.
(* Goal: @eq (@Tpoint Tn) A B *)
    repeat split; auto.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
    induction H15.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
      assert(Bet O B' E').
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(project_preserves_bet O E' E E' O B E O B' E'); auto.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
      assert(Bet O AB A).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(project_preserves_bet O E E' A O B' E' O AB A); auto.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
      induction H17.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
        left.
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(between_exchange4 _ _ A); auto.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply(l5_3 O AB E A); auto.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
    assert(Bet O E' B').
(* Goal: @eq (@Tpoint Tn) A B *)
      apply(project_preserves_bet O E' E E' O E B O E' B'); auto.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
    assert(Bet O A AB).
(* Goal: @eq (@Tpoint Tn) A B *)
      apply(project_preserves_bet O E E' A O E' B' O A AB); auto.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
    induction H17.
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
(* Goal: or (@Bet Tn O AB E) (@Bet Tn O E AB) *)
      assert(Bet O E AB \/ Bet O AB E).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(l5_1 O A E AB); auto.
(* Goal: @eq (@Tpoint Tn) A A *)
      tauto.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    right.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply (between_exchange4 O E A AB); auto.
Qed.

Lemma pos_not_neg : forall O E A, Ps O E A -> ~Ng O E A.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
    intro.
(* Goal: False *)
    unfold Ps in H.
(* Goal: False *)
    unfold Ng in H0.
(* Goal: False *)
    unfold Out in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: False *)
    induction H4.
(* Goal: False *)
(* Goal: False *)
      apply H.
(* Goal: @eq (@Tpoint Tn) A O *)
(* Goal: False *)
      apply (between_equality _ _ E); Between.
(* Goal: False *)
    apply H1.
(* Goal: @eq (@Tpoint Tn) E O *)
    apply (between_equality _ _ A); Between.
Qed.

Lemma neg_not_pos : forall O E A, Ng O E A -> ~Ps O E A.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
    intro.
(* Goal: False *)
    unfold Ps in H0.
(* Goal: @Ps Tn O E MA *)
    unfold Ng in H.
(* Goal: False *)
    unfold Out in H0.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: False *)
    induction H2.
(* Goal: False *)
(* Goal: False *)
      apply H0.
(* Goal: @eq (@Tpoint Tn) A O *)
(* Goal: False *)
      apply (between_equality _ _ E); Between.
(* Goal: False *)
    apply H1.
(* Goal: @eq (@Tpoint Tn) E O *)
    apply (between_equality _ _ A); Between.
Qed.

Lemma opp_pos_neg : forall O E E' A MA, Ps O E A ->  Opp O E E' A MA -> Ng O E MA.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ps Tn O E MA *)
    assert(HH:=opp_midpoint O E E' A MA H0).
(* Goal: @Ng Tn O E mA *)
    unfold Ng.
(* Goal: False *)
    unfold Ps in H.
(* Goal: False *)
    unfold Out in H.
(* Goal: @Out Tn O MA E *)
    unfold Midpoint in HH.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @eq (@Tpoint Tn) A B *)
    repeat split; auto.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      subst MA.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      apply cong_identity in H2.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      contradiction.
(* Goal: False *)
    induction H4.
(* Goal: @Bet Tn MA O E *)
(* Goal: @Bet Tn MA O E *)
      apply(outer_transitivity_between MA O A E); Between.
(* Goal: @Bet Tn MA O E *)
    apply(between_inner_transitivity MA O E A); Between.
Qed.

Lemma opp_neg_pos : forall O E E' A MA, Ng O E A ->  Opp O E E' A MA -> Ps O E MA.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ps Tn O E MA *)
    assert(HH:=opp_midpoint O E E' A MA H0).
(* Goal: @Ps Tn O E MA *)
    unfold Ng in H.
(* Goal: @Ps Tn O E MA *)
    unfold Ps.
(* Goal: @Out Tn O MA E *)
    unfold Midpoint in HH.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Out Tn O MA E *)
    apply l6_6.
(* Goal: @Out Tn O E MA *)
    unfold Out.
(* Goal: @eq (@Tpoint Tn) A B *)
    repeat split; auto.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      subst MA.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      apply cong_identity in H2.
(* Goal: False *)
(* Goal: or (@Bet Tn O E MA) (@Bet Tn O MA E) *)
      contradiction.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply (l5_2 A O E MA); auto.
Qed.

Lemma ltP_ar2 : forall O E E' A B, LtP O E E' A B -> Ar2 O E E' A B A.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold LtP in H.
(* Goal: @Ar2 Tn O E E' A B A *)
    ex_and H D.
(* Goal: @Ar2 Tn O E E' A B A *)
    apply diff_ar2 in H.
(* Goal: @Ar2 Tn O E E' A B A *)
    unfold Ar2 in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @eq (@Tpoint Tn) A B *)
    repeat split; auto.
Qed.

Lemma ltP_neq : forall O E E' A B, LtP O E E' A B -> A <> B.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    assert(HH:=ltP_ar2 O E E' A B H).
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold Ar2 in HH.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
    unfold LtP in H.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
    intro.
(* Goal: or (@LtP Tn O E E' A B) (@eq (@Tpoint Tn) A B) *)
    subst B.
(* Goal: False *)
    ex_and H OO.
(* Goal: False *)
    assert(OO=O).
(* Goal: @eq (@Tpoint Tn) OO O *)
(* Goal: False *)
      apply (diff_uniqueness O E E' A A).
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
        assumption.
(* Goal: @Diff Tn O E E' A A O *)
(* Goal: False *)
      apply diff_null; Col.
(* Goal: False *)
    subst OO.
(* Goal: False *)
    unfold Ps in H4.
(* Goal: False *)
    unfold Out in H4.
(* Goal: @eq (@Tpoint Tn) A A *)
    tauto.
Qed.

Lemma leP_refl : forall O E E' A, LeP O E E' A A.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    right.
(* Goal: @eq (@Tpoint Tn) A A *)
    tauto.
Qed.

Lemma ltP_sum_pos : forall O E E' A B C , Ps O E B -> Sum O E E' A B C -> LtP O E E' A C.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @LtP Tn O E E' A C *)
    unfold LtP.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
    exists B.
(* Goal: @eq (@Tpoint Tn) A B *)
    split; auto.
(* Goal: @Diff Tn O E E' C A B *)
    apply sum_diff in H0.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    assumption.
Qed.

Lemma pos_opp_neg : forall O E E' A mA, Ps O E A -> Opp O E E' A mA -> Ng O E mA.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ng Tn O E mA *)
    assert(Ar2 O E E' mA A O).
(* Goal: @Ar2 Tn O E E' mA A O *)
(* Goal: @Ng Tn O E mA *)
      unfold Opp in H0.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply sum_ar2; auto.
(* Goal: @Ng Tn O E mA *)
    unfold Ar2 in H1.
(* Goal: @Ng Tn O E mA *)
    apply opp_midpoint in H0.
(* Goal: @Ng Tn O E mA *)
    unfold Midpoint in H0.
(* Goal: False *)
    unfold Ps in H.
(* Goal: False *)
    unfold Out in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: @Ng Tn O E mA *)
    unfold Ng.
(* Goal: and (@Diff Tn O E E' C A dCA) (@Ps Tn O E dCA) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
    repeat split.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
      intro.
(* Goal: False *)
(* Goal: not (@eq (@Tpoint Tn) E O) *)
(* Goal: @Bet Tn mA O E *)
      subst mA.
(* Goal: False *)
(* Goal: False *)
      apply H.
(* Goal: @eq (@Tpoint Tn) A O *)
(* Goal: not (@eq (@Tpoint Tn) E O) *)
(* Goal: @Bet Tn mA O E *)
      apply cong_identity in H5.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assumption.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @Bet Tn mA O E *)
    induction H7.
(* Goal: @Bet Tn mA O E *)
(* Goal: @Bet Tn mA O E *)
      apply(outer_transitivity_between mA O A E); Between.
(* Goal: @Bet Tn mA O E *)
    apply between_symmetry.
(* Goal: @Bet Tn E O mA *)
    apply(between_exchange3 A E O mA); Between.
Qed.

Lemma diff_pos_diff_neg : forall O E E' A B AmB BmA,
  Diff O E E' A B AmB -> Diff O E E' B A BmA -> Ps O E AmB -> Ng O E BmA.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @Ng Tn O E BmA *)
    assert(Opp O E E' AmB BmA).
(* Goal: @eq (@Tpoint Tn) A B *)
      apply (diff_opp O E E' A B); auto.
(* Goal: @eq (@Tpoint Tn) A B *)
    eapply (pos_opp_neg O E E' AmB); auto.
Qed.


Lemma not_pos_and_neg : forall O E A, ~(Ps O E A /\ Ng O E A).
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: not (and (@Ps Tn O E A) (@Ng Tn O E A)) *)
    intro.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: False *)
    unfold Ps in H.
(* Goal: False *)
    unfold Ng in H0.
(* Goal: False *)
    unfold Out in H.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    clean_duplicated_hyps.
(* Goal: False *)
    induction H4.
(* Goal: False *)
(* Goal: False *)
      apply H.
      apply (between_equality _  _ E); Between.
(* Goal: False *)
    apply H3.
    apply (between_equality _  _ A); Between.
Qed.

Lemma leP_asym : forall O E E' A B, LeP O E E' A B -> LeP O E E' B A -> A = B.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @LeP Tn O E E' C Z *)
    unfold LeP in *.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    induction H; induction H0.
(* Goal: @LtP Tn O E E' C Z *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      unfold LtP in *.
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
      ex_and H BmA.
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
      ex_and H0 AmB.
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
      assert(HH:=diff_pos_diff_neg O E E' A B AmB BmA H0 H H2).
      assert(HT:=diff_pos_diff_neg O E E' B A BmA AmB  H H0 H1).
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
      apply False_ind.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
      assert(HN:=not_pos_and_neg O E AmB).
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
(* Goal: @eq (@Tpoint Tn) A B *)
      apply HN.
(* Goal: @eq (@Tpoint Tn) A B *)
      split; auto.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @eq (@Tpoint Tn) A B *)
      auto.
(* Goal: @eq (@Tpoint Tn) A B *)
    auto.
Qed.

Lemma leP_trans : forall O E E' A B C, LeP O E E' A B -> LeP O E E' B C -> LeP O E E' A C.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @LeP Tn O E E' C Z *)
    unfold LeP in *.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    induction H; induction H0.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left.
(* Goal: @LtP Tn O E E' C Z *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      unfold LtP in *.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      ex_and H dBA.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      ex_and H0 dCB.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      assert(Ar2 O E E' B A dBA).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply diff_ar2; auto.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      assert(Ar2 O E E' C B dCB).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply diff_ar2; auto.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      unfold Ar2 in *.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      spliter.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      clean_duplicated_hyps.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      assert(HH:= sum_exists O E E' H3 dBA dCB H10 H7).
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      ex_and HH dCA.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' C A D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      exists dCA.
(* Goal: and (@Diff Tn O E E' C A dCA) (@Ps Tn O E dCA) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      assert(HH:= sum_diff_diff_b O E E' A B C dBA dCB dCA H H0).
(* Goal: and (@Diff Tn O E E' C A dCA) (@Ps Tn O E dCA) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      split.
(* Goal: @Diff Tn O E E' C A dCA *)
(* Goal: @Ps Tn O E dCA *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
        apply HH.
(* Goal: @eq (@Tpoint Tn) A B *)
        apply sum_comm; auto.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply(sum_pos_pos O E E' dBA dCB); auto.
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
      subst C.
(* Goal: @eq (@Tpoint Tn) A B *)
      left; auto.
(* Goal: or (@LtP Tn O E E' A B) (@eq (@Tpoint Tn) A B) *)
      subst B.
(* Goal: @eq (@Tpoint Tn) A B *)
      left; auto.
(* Goal: or (@LtP Tn O E E' A C) (@eq (@Tpoint Tn) A C) *)
    subst C.
(* Goal: or (@LtP Tn O E E' A B) (@eq (@Tpoint Tn) A B) *)
    subst B.
(* Goal: @eq (@Tpoint Tn) A B *)
    right; auto.
Qed.

(* sum_preserves leP : a <= x /\ b <= y => a + b <= x + y *)

Lemma leP_sum_leP : forall O E E' A B C X Y Z,
  LeP O E E' A X -> LeP O E E' B Y -> Sum O E E' A B C -> Sum O E E' X Y Z ->
  LeP O E E' C Z.
Proof.
(* Goal: forall (O E E' A B C X Y Z : @Tpoint Tn) (_ : @LeP Tn O E E' A X) (_ : @LeP Tn O E E' B Y) (_ : @Sum Tn O E E' A B C) (_ : @Sum Tn O E E' X Y Z), @LeP Tn O E E' C Z *)
    intros.
(* Goal: @LeP Tn O E E' C Z *)
    unfold LeP in *.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    assert(Ar2 O E E' A B C).
(* Goal: @eq (@Tpoint Tn) A B *)
      apply sum_ar2; auto.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    assert(Ar2 O E E' X Y Z).
(* Goal: @eq (@Tpoint Tn) A B *)
      apply sum_ar2; auto.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    unfold Ar2 in *.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    spliter.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    clean_duplicated_hyps.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    induction H; induction H0.
(* Goal: @LtP Tn O E E' C Z *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      unfold LtP in *.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and H dXA.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and H0 dYB.
      assert(HH:= diff_exists O E E' Z C  H3 H7 H10).
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and HH dZC.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      exists dZC.
(* Goal: @eq (@Tpoint Tn) A B *)
      split; auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(Sum O E E' dXA dYB dZC).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(sum_diff2_diff_sum2_b O E E' A B C X Y Z dXA dYB dZC H1 H2 H H0); auto.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply(sum_pos_pos O E E' dXA dYB); auto.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      subst Y.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left.
(* Goal: @LtP Tn O E E' C Z *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      unfold LtP in *.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and H dXA.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(HH:=diff_exists O E E' Z C H3 H7 H10).
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and HH dZC.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      exists dZC.
(* Goal: @eq (@Tpoint Tn) A B *)
      split; auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(Sum O E E' dXA O dZC).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(sum_diff2_diff_sum2_b O E E' A B C X B Z dXA O dZC); auto.
(* Goal: @eq (@Tpoint Tn) A B *)
        apply diff_null; auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(dXA = dZC).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(sum_A_O_eq O E E'); auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      subst dXA.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assumption.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      subst X.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      left.
(* Goal: @LtP Tn O E E' C Z *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      unfold LtP in *.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and H0 dYB.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(HH:=diff_exists O E E' Z C H3 H7 H10).
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      ex_and HH dZC.
(* Goal: @ex (@Tpoint Tn) (fun D : @Tpoint Tn => and (@Diff Tn O E E' Z C D) (@Ps Tn O E D)) *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      exists dZC.
(* Goal: @eq (@Tpoint Tn) A B *)
      split; auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(Sum O E E' O dYB dZC).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(sum_diff2_diff_sum2_b O E E' A B C A Y Z O dYB dZC); auto.
(* Goal: @eq (@Tpoint Tn) A B *)
        apply diff_null; auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assert(dYB = dZC).
(* Goal: @eq (@Tpoint Tn) A B *)
        apply(sum_O_B_eq O E E'); auto.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      subst dYB.
(* Goal: @Ps Tn O E dZC *)
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
      assumption.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    subst X.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    subst Y.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
    right.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply(sum_uniqueness O E E' A B); auto.
Qed.

Lemma square_pos : forall O E E' A A2,
  O <> A -> Prod O E E' A A A2 -> Ps O E A2.
Proof.
(* Goal: forall (O E E' A A2 : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O A)) (_ : @Prod Tn O E E' A A A2), @Ps Tn O E A2 *)
intros O E E' A A2 HDiff HA2.
(* Goal: @LeP Tn O E E' AC BC *)
assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
destruct (opp_exists O E E' HNC A) as [MA HMA]; Col.
(* Goal: @Ps Tn O E A2 *)
assert (HElim := HMA); apply pos_null_neg in HElim.
(* Goal: @Ps Tn O E A2 *)
elim HElim; clear HElim; intro HElim; [apply prod_pos_pos with E' A A; auto|].
elim HElim; clear HElim; intro HPs;
[intuition|apply prod_pos_pos with E' MA MA; auto].
(* Goal: @Ps Tn O E IA *)
destruct (opp_exists O E E' HNC E) as [ME HME]; Col.
(* Goal: @eq (@Tpoint Tn) A B *)
apply prod_assoc1 with A ME A; auto; [|apply prod_comm]; apply opp_prod; auto.
(* Goal: @Opp Tn O E E' MA A *)
apply opp_comm; Col.
Qed.

(** Lemma 14.40 states that we have an ordered field. *)

Lemma col_pos_or_neg : forall O E X,
  O <> E -> O <> X -> Col O E X -> Ps O E X \/ Ng O E X.
Proof.
(* Goal: forall (O E X : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O E)) (_ : not (@eq (@Tpoint Tn) O X)) (_ : @Col Tn O E X), or (@Ps Tn O E X) (@Ng Tn O E X) *)
intros O E X HOE HOX HCol.
(* Goal: or (@Ps Tn O E X) (@Ng Tn O E X) *)
unfold Ps, Ng, Out.
(* Goal: not (and (not (@eq (@Tpoint Tn) O O)) (and (not (@eq (@Tpoint Tn) E O)) (or (@Bet Tn O O E) (@Bet Tn O E O)))) *)
unfold Col in HCol; intuition.
Qed.

Lemma ltP_neg : forall O E E' A, LtP O E E' A O -> Ng O E A.
Proof.
(* Goal: forall (O E E' A : @Tpoint Tn) (_ : @LtP Tn O E E' A O), @Ng Tn O E A *)
intros O E E' A HLt.
(* Goal: @Ng Tn O E A *)
destruct HLt as [MA [HDiff HPs]].
(* Goal: @eq (@Tpoint Tn) A B *)
apply opp_pos_neg with E' MA; auto.
(* Goal: @eq (@Tpoint Tn) A B *)
apply diff_O_A_opp; apply sum_diff; apply sum_comm; try apply diff_sum; auto.
(* Goal: not (@Col Tn O E E') *)
unfold Diff, Opp, Sum, Ar2 in HDiff; destruct HDiff as [MB HXMY]; spliter; Col.
Qed.

Lemma ps_le : forall O E E' X,
  ~ Col O E E' -> Bet O X E \/ Bet O E X -> LeP O E E' O X.
Proof.
(* Goal: forall (O E E' X : @Tpoint Tn) (_ : not (@Col Tn O E E')) (_ : or (@Bet Tn O X E) (@Bet Tn O E X)), @LeP Tn O E E' O X *)
intros O E E' X HNC HBet.
(* Goal: @LeP Tn O E E' O X *)
elim (eq_dec_points O X); intro HOX; [right; auto|left].
(* Goal: @LtP Tn O E E' O X *)
exists X; split; [apply diff_A_O; induction HBet; Col|].
(* Goal: @Ps Tn O E X *)
assert_diffs; repeat (split; Col).
Qed.

Lemma lt_diff_ps : forall O E E' X Y XMY,
  Col O E X -> Col O E Y -> LtP O E E' Y X -> Diff O E E' X Y XMY -> Ps O E XMY.
Proof.
(* Goal: forall (O E E' X Y XMY : @Tpoint Tn) (_ : @Col Tn O E X) (_ : @Col Tn O E Y) (_ : @LtP Tn O E E' Y X) (_ : @Diff Tn O E E' X Y XMY), @Ps Tn O E XMY *)
intros O E E' X Y XMY HCol1 HCol2 HLt HXMY.
(* Goal: @Ps Tn O E XMY *)
destruct HLt as [XMY' [HDiff HPs]].
(* Goal: @eq (@Tpoint Tn) A B *)
apply (diff_uniqueness _ _ _ _ _ XMY) in HDiff; treat_equalities; auto.
Qed.

Lemma col_2_le_or_ge : forall O E E' A B,
  ~ Col O E E' -> Col O E A -> Col O E B -> LeP O E E' A B \/ LeP O E E' B A.
Proof.
(* Goal: forall (O E E' A B : @Tpoint Tn) (_ : not (@Col Tn O E E')) (_ : @Col Tn O E A) (_ : @Col Tn O E B), or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
intros O E E' A B HNC HColA HColB.
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
assert (HDiff1 : O <> E) by (assert_diffs; auto).
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
elim (eq_dec_points A B); intro HDiff2; treat_equalities; [left; right; auto|].
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
destruct (diff_exists O E E' B A) as [D HD]; Col.
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
assert (HColD : Col O E D) by (apply diff_ar2 in HD; unfold Ar2 in *; spliter; Col).
assert (HDiff3 : O <> D)
  by (intro; treat_equalities; apply diff_null_eq in HD; intuition).
(* Goal: @eq (@Tpoint Tn) A B *)
apply col_pos_or_neg in HColD; auto.
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
elim HColD; clear HColD; intro HNgD; [left; left; exists D; auto|].
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
destruct (diff_exists O E E' A B) as [MD HMD]; Col.
(* Goal: @eq (@Tpoint Tn) A B *)
right; left; exists MD; split; auto; apply opp_neg_pos with E' D; auto.
(* Goal: @eq (@Tpoint Tn) A B *)
apply diff_opp with B A; auto.
Qed.

Lemma compatibility_of_sum_with_order : forall O E E' A B C APC BPC,
  LeP O E E' A B -> Sum O E E' A C APC -> Sum O E E' B C BPC ->
  LeP O E E' APC BPC.
Proof.
(* Goal: forall (O E E' A B C APC BPC : @Tpoint Tn) (_ : @LeP Tn O E E' A B) (_ : @Sum Tn O E E' A C APC) (_ : @Sum Tn O E E' B C BPC), @LeP Tn O E E' APC BPC *)
intros O E E' A B C APC BPC HLe HAPC HBPC.
(* Goal: @LeP Tn O E E' APC BPC *)
elim HLe; clear HLe; intro HLe.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
(* Goal: @eq (@Tpoint Tn) A B *)
  left; destruct HLe as [D [HDiff HPs]]; exists D; split; auto.
  assert (HNC : ~ Col O E E')
    by (apply diff_ar2 in HDiff; unfold Ar2 in *; spliter; Col).
  apply sum_diff; apply diff_sum in HDiff;
  apply sum_assoc_1 with C A B; auto;
(* Goal: @eq (@Tpoint Tn) A B *)
  apply sum_comm; auto.
  }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
(* Goal: @LeP Tn O E E' C B *)
  treat_equalities.
(* Goal: @LeP Tn O E E' APC BPC *)
  assert (APC = BPC) by (apply sum_uniqueness with O E E' A C; auto).
(* Goal: @LeP Tn O E E' APC BPC *)
  treat_equalities; apply leP_refl.
  }
Qed.

Lemma compatibility_of_prod_with_order : forall O E E' A B AB,
  LeP O E E' O A -> LeP O E E' O B -> Prod O E E' A B AB ->
  LeP O E E' O AB.
Proof.
(* Goal: forall (O E E' A B AB : @Tpoint Tn) (_ : @LeP Tn O E E' O A) (_ : @LeP Tn O E E' O B) (_ : @Prod Tn O E E' A B AB), @LeP Tn O E E' O AB *)
intros O E E' A B AB HLeA HLeB HAB.
elim HLeA; clear HLeA; intro HLeA;
elim HLeB; clear HLeB; intro HLeB; treat_equalities;
try (apply prod_O_l_eq in HAB); try (apply prod_O_r_eq in HAB);
treat_equalities; try (apply leP_refl).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColB : Col O E B) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' O AB *)
assert (HColAB : Col O E AB) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' O AB *)
left; exists AB; split; try (apply diff_A_O); Col.
(* Goal: @Ps Tn O E AB *)
destruct HLeA as [A' [HDiff1 HPsA]]; destruct HLeB as [B' [HDiff2 HPsB]].
assert (A = A')
  by (apply diff_uniqueness with O E E' A O; auto; apply diff_A_O; Col).
assert (B = B')
  by (apply diff_uniqueness with O E E' B O; auto; apply diff_A_O; Col).
(* Goal: @eq (@Tpoint Tn) A B *)
treat_equalities; apply prod_pos_pos with E' A B; auto.
Qed.

Lemma pos_inv_pos : forall O E E' A IA,
  O <> A -> LeP O E E' O A -> Prod O E E' IA A E -> LeP O E E' O IA.
Proof.
(* Goal: forall (O E E' A IA : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) O A)) (_ : @LeP Tn O E E' O A) (_ : @Prod Tn O E E' IA A E), @LeP Tn O E E' O IA *)
intros O E E' A IA HOA HLe HIA.
(* Goal: @LeP Tn O E E' O IA *)
elim HLe; clear HLe; intro HLe; treat_equalities; [|intuition].
(* Goal: @LeP Tn O E E' AC BC *)
assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' O IA *)
assert (HColIA : Col O E IA) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' O IA *)
destruct (diff_exists O E E' IA O) as [IA' HIA']; Col.
(* Goal: @LeP Tn O E E' O IA *)
assert (IA = IA') by (apply diff_uniqueness with O E E' IA O; auto; apply diff_A_O; Col).
(* Goal: @LeP Tn O E E' O IA *)
treat_equalities; left; exists IA; split; auto; clear HIA'.
(* Goal: @Ps Tn O E IA *)
destruct HLe as [A' [HDiff HPs1]].
(* Goal: @Ps Tn O E IA *)
assert (A = A') by (apply diff_uniqueness with O E E' A O; auto; apply diff_A_O; Col).
(* Goal: @Ps Tn O E IA *)
treat_equalities; clear HDiff; destruct (opp_exists O E E' HNC IA) as [MIA HMIA]; Col.
(* Goal: @Ps Tn O E IA *)
assert (HElim := HMIA); apply pos_null_neg in HElim.
(* Goal: @eq (@Tpoint Tn) A B *)
elim HElim; clear HElim; intro HElim; auto.
(* Goal: @LeP Tn O E E' C B *)
elim HElim; clear HElim; intro HPs2; treat_equalities.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  assert (O = E)
    by (apply prod_uniqueness with O E E' O A; auto; apply prod_0_l; Col).
(* Goal: not (and (not (@eq (@Tpoint Tn) O O)) (and (not (@eq (@Tpoint Tn) E O)) (or (@Bet Tn O O E) (@Bet Tn O E O)))) *)
  treat_equalities; intuition.
  }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
(* Goal: @Ps Tn O E IA *)
  destruct (opp_exists O E E' HNC E) as [ME HME]; Col.
(* Goal: @Ps Tn O E IA *)
  assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @Ps Tn O E IA *)
  assert (HProd1 : Prod O E E' IA ME MIA) by (apply opp_prod; auto).
(* Goal: @Ps Tn O E IA *)
  assert (HProd2 : Prod O E E' MIA A ME).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    apply prod_assoc1 with ME IA E; auto;
    apply prod_comm; auto; apply prod_1_l; Col.
    }
(* Goal: @Ps Tn O E IA *)
  assert (HFalse : Ps O E ME) by (apply prod_pos_pos with E' MIA A; auto).
(* Goal: @eq (@Tpoint Tn) A B *)
  apply opp_pos_neg with O E E' ME E in HFalse; try apply opp_comm; auto.
(* Goal: @Ps Tn O E IA *)
  exfalso; apply neg_not_pos in HFalse; apply HFalse.
(* Goal: @Ps Tn O E E *)
  assert_diffs; repeat (split; Between).
  }
Qed.

Unset Regular Subst Tactic.

Lemma le_pos_prod_le : forall O E E' A B C AC BC,
  LeP O E E' A B -> LeP O E E' O C ->
  Prod O E E' A C AC -> Prod O E E' B C BC ->
  LeP O E E' AC BC.
Proof.
(* Goal: forall (O E E' A B C AC BC : @Tpoint Tn) (_ : @LeP Tn O E E' A B) (_ : @LeP Tn O E E' O C) (_ : @Prod Tn O E E' A C AC) (_ : @Prod Tn O E E' B C BC), @LeP Tn O E E' AC BC *)
intros O E E' A B C AC BC HALeB HPsC HAC HBC.
(* Goal: @LeP Tn O E E' AC BC *)
assert (HNC : ~ Col O E E') by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColA : Col O E A) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColB : Col O E B) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColC : Col O E C) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColAC : Col O E AC) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
assert (HColBC : Col O E BC) by (unfold Prod, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AC BC *)
destruct (diff_exists O E E' BC AC) as [BCMAC HBCMAC]; Col.
apply compatibility_of_sum_with_order with O BCMAC AC;
try apply sum_O_B; try (apply sum_comm; try apply diff_sum); Col.
(* Goal: @LeP Tn O E E' O BCMAC *)
destruct (diff_exists O E E' B A) as [BMA HBMA]; Col.
assert (HColBMA : Col O E BMA)
  by (apply diff_ar2 in HBMA; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' O BCMAC *)
destruct (prod_exists O E E' HNC BMA C) as [BCMAC' HBCMAC']; Col.
(* Goal: @LeP Tn O E E' O BCMAC *)
assert (H : Diff O E E' BC AC BCMAC').
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  apply sum_diff; apply diff_sum in HBMA;
(* Goal: @eq (@Tpoint Tn) A B *)
  apply distr_r with A BMA C B; auto.
  }
(* Goal: @LeP Tn O E E' O BCMAC *)
assert (BCMAC = BCMAC') by (apply diff_uniqueness with O E E' BC AC; auto).
clear H; treat_equalities;
(* Goal: @eq (@Tpoint Tn) A B *)
apply compatibility_of_prod_with_order with BMA C; auto.
(* Goal: @LeP Tn O E E' C B *)
destruct (opp_exists O E E' HNC A) as [MA HMA]; Col.
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColMA : Col O E MA) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
apply compatibility_of_sum_with_order with A B MA; auto;
try (apply diff_sum; apply diff_O_A; Col).
(* Goal: @Sum Tn O E E' B MA BMA *)
apply diff_O_A in HMA; Col; apply diff_sum in HBMA; apply diff_sum in HMA.
(* Goal: @Sum Tn O E E' B MA BMA *)
apply sum_assoc_1 with BMA A O; auto; try apply sum_A_O; Col.
(* Goal: @eq (@Tpoint Tn) A B *)
apply sum_comm; auto.
Qed.

Lemma bet_lt12_le23 : forall O E E' A B C,
  Bet A B C -> LtP O E E' A B -> LeP O E E' B C.
Proof.
(* Goal: forall (O E E' A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @LtP Tn O E E' B A), @LeP Tn O E E' C A *)
intros O E E' A B C HBet HLt.
assert (HNC : ~ Col O E E')
  by (destruct HLt as [D [H H']]; apply diff_ar2 in H; unfold Ar2 in *; spliter; Col).
(* Goal: or (@LeP Tn O E E' A B) (@LeP Tn O E E' B A) *)
assert (HDiff1 : O <> E) by (assert_diffs; auto).
(* Goal: @LeP Tn O E E' C B *)
elim (eq_dec_points B C); intro HDiff2; [right; auto|].
assert (HDiff3 : A <> B) by (apply ltP_neq with O E E'; auto).
assert (HColA : Col O E A)
  by (destruct HLt as [D [H H']]; apply diff_ar2 in H; unfold Ar2 in *; spliter; Col).
assert (HColB : Col O E B)
  by (destruct HLt as [D [H H']]; apply diff_ar2 in H; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
assert (HColC : Col O E C) by (assert_diffs; assert_cols; ColR).
destruct (diff_exists O E E' C B) as [CMB HCMB]; Col.
elim (eq_dec_points O A); intro HDiff4; elim (eq_dec_points O B); intro HDiff5;
elim (eq_dec_points O C); intro HDiff6; treat_equalities;
[intuition|intuition|intuition| |right; auto| | |].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  destruct HLt as [B' [HB' HPs]].
(* Goal: @Ps Tn O E AB *)
  assert (B = B') by (apply diff_uniqueness with O E E' B O; auto; apply diff_A_O; Col).
(* Goal: @eq (@Tpoint Tn) A B *)
  treat_equalities; left; exists CMB; split; auto.
  split; try (intro; treat_equalities; apply HDiff2; apply eq_sym;
              apply diff_null_eq with CMB E E'; auto).
  split; auto; apply diff_sum in HCMB; apply sum_cong in HCMB;
  Col; apply plgf_bet in HCMB.
  do 3 (try (elim HCMB; clear HCMB; intro HCMB;
             try destruct HCMB as [HBet1 HBet2])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    exfalso; apply HDiff5; apply between_equality with C; Between.
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    exfalso; apply HDiff2; apply between_equality with O; Between.
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    destruct HPs as [H [H' HElim]]; clear H; clear H'.
    elim HElim; clear HElim; intro HElim; [eBetween|].
    elim (l5_3 O CMB E B); Between.
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    destruct HPs as [H [H' HElim]]; clear H; clear H'.
    elim HElim; clear HElim; intro HElim; [|eBetween].
    elim (l5_2 O B CMB E); eBetween.
    }
  }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  apply ltP_neg in HLt; apply ps_le; Col.
(* Goal: or (@LtP Tn O E E' C Z) (@eq (@Tpoint Tn) C Z) *)
  unfold Ng in *; spliter.
  elim (l5_2 A O C E); Between.
  }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  rename CMB into MB.
  left; exists MB; split; auto; apply opp_neg_pos with E' B;
(* Goal: @eq (@Tpoint Tn) A B *)
  try apply diff_O_A_opp; auto.
  apply col_pos_or_neg in HColB; try (intro; treat_equalities; Col).
  elim HColB; clear HColB; intro HPsB; auto; exfalso.
  apply col_pos_or_neg in HColA; try (intro; treat_equalities; Col).
  elim HColA; clear HColA; [intro HPsA|intro HNgA].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
    elim (eq_dec_points A BMA); intro HDiff6; treat_equalities;
    [apply l14_36_a in HBMA; try apply out_trivial; auto;
     apply HDiff3; apply between_equality with O; Between|].
    apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
    do 3 (try (elim HBMA; clear HBMA; intro HBMA;
               try destruct HBMA as [HBet1 HBet2])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      apply HDiff5; apply between_equality with A; Between.
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
(* Goal: @eq (@Tpoint Tn) A B *)
      apply not_pos_and_neg with O E BMA; split; auto.
      split; try (intro; treat_equalities; apply O_not_positive with BMA E; auto).
      split; auto; destruct HPsB as [H [H' HElim]]; clear H; clear H'.
      elim HElim; clear HElim; intro HElim; eBetween.
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      apply HDiff3; apply between_equality with O; Between.
(* Goal: @eq (@Tpoint Tn) A B *)
      apply between_symmetry; apply outer_transitivity_between2 with BMA; auto.
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      apply HDiff3; apply between_equality with O; Between.
      apply outer_transitivity_between2 with BMA; Between.
      }
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
(* Goal: @eq (@Tpoint Tn) A B *)
    apply not_pos_and_neg with O E A; split; auto.
    do 2 (split; auto); destruct HPsB as [H [H' HElim]]; clear H; clear H'.
    elim HElim; clear HElim; intro HBet'; [|eBetween].
    elim (l5_2 O B A E); eBetween.
    }
  }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  left; exists CMB; split; auto; apply diff_sum in HCMB; assert (HCMB' := HCMB).
  split; try (intro; treat_equalities; apply HDiff2;
              apply sum_uniqueness with CMB E E' B CMB; auto; apply sum_A_O; Col).
  split; auto; apply sum_cong in HCMB; Col; apply plgf_bet in HCMB.
  apply col_pos_or_neg in HColA; try (intro; treat_equalities; Col).
  apply col_pos_or_neg in HColB; try (intro; treat_equalities; Col).
  elim HColA; clear HColA; [intro HPsA|intro HNgA].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    do 3 (try (elim HCMB; clear HCMB; intro HCMB;
               try destruct HCMB as [HBet1 HBet2])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      elim HColB; clear HColB; [intro HPsB|intro HNgB].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
        destruct HPsB as [H [H' HElim2]]; clear H; clear H'.
        elim HElim1; clear HElim1; intro HBet3;
        elim HElim2; clear HElim2; intro HBet4.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          elim (l5_3 O A B E); Between; intro HBet5.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet6 : Bet O B C) by eBetween.
            exfalso; apply HDiff5; apply between_equality with C; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
            elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
            [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
             apply HDiff3; apply between_equality with O; Between|].
            apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
            do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                       try destruct HBMA as [HBet6 HBet7])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              exfalso; apply HDiff5; apply between_equality with A; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              destruct HPsBMA as [HDiff8 [H HElim]]; clear H.
              elim HElim; clear HElim; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
                {
                assert (HBet9 : Bet E O B)
                  by (apply outer_transitivity_between2 with BMA; Between).
                exfalso; apply HDiff5; apply between_equality with E; Between.
                }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
                {
                assert (HBet9 : Bet E O B) by eBetween.
                exfalso; apply HDiff5; apply between_equality with E; Between.
                }
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O A B)
                by (apply outer_transitivity_between2 with BMA; Between).
              exfalso; apply HDiff3; apply between_equality with O; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O A B) by eBetween.
              exfalso; apply HDiff3; apply between_equality with O; Between.
              }
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet5 : Bet O B C) by eBetween.
          exfalso; apply HDiff5; apply between_equality with C; Between.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
           apply HDiff3; apply between_equality with O; eBetween|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet5 HBet6])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O B A) by eBetween.
            exfalso; apply HDiff5; apply between_equality with A; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H';
            elim HElim; clear HElim; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              elim (l5_3 O B BMA E); Between; intro HBet8; exfalso;
              [apply HDiff5; apply between_equality with BMA|
               apply HDiff8; apply between_equality with B]; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O B BMA) by eBetween.
              exfalso; apply HDiff5; apply between_equality with BMA; Between.
              }
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet O B A) by eBetween.
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet O B A) by eBetween.
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
           apply HDiff3; apply between_equality with O; eBetween|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet5 HBet6])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet A O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with A; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H';
            elim HElim; clear HElim; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet BMA O E) by eBetween.
              exfalso; apply HDiff8; apply between_equality with E; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet BMA O E) by eBetween.
              exfalso; apply HDiff1; apply between_equality with BMA; Between.
              }
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet B A C) by eBetween.
            exfalso; apply HDiff3; apply between_equality with C; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet B A C) by eBetween.
            exfalso; apply HDiff3; apply between_equality with C; Between.
            }
          }
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        exfalso; apply neg_not_pos in HNgB; apply HNgB; clear HNgB.
        do 2 (split; auto).
        destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
        elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
        [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
         apply HDiff3; apply between_equality with O; eBetween|].
        apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
        do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                   try destruct HBMA as [HBet3 HBet4])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet5 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet6;
          elim HElim2; clear HElim2; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet5 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet6;
          elim HElim2; clear HElim2; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet5; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet5; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }
        }
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      elim HColB; clear HColB; [intro HPsB|intro HNgB].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
        destruct HPsB as [H [H' HElim2]]; clear H; clear H'.
        elim HElim1; clear HElim1; intro HBet3;
        elim HElim2; clear HElim2; intro HBet4.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          elim (l5_3 O A B E); Between; intro HBet5.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet6 : Bet O B C) by eBetween.
            exfalso; apply HDiff2; apply between_equality with O; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
            elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
            [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
             apply HDiff3; apply between_equality with O; Between|].
            apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
            do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                       try destruct HBMA as [HBet6 HBet7])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              exfalso; apply HDiff5; apply between_equality with A; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              destruct HPsBMA as [HDiff8 [H HElim]]; clear H.
              elim HElim; clear HElim; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
                {
                assert (HBet9 : Bet E O B)
                  by (apply outer_transitivity_between2 with BMA; Between).
                exfalso; apply HDiff5; apply between_equality with E; Between.
                }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
                {
                assert (HBet9 : Bet E O B) by eBetween.
                exfalso; apply HDiff5; apply between_equality with E; Between.
                }
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O A B)
                by (apply outer_transitivity_between2 with BMA; Between).
              exfalso; apply HDiff3; apply between_equality with O; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O A B) by eBetween.
              exfalso; apply HDiff3; apply between_equality with O; Between.
              }
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet5 : Bet O B C) by eBetween.
          exfalso; apply HDiff2; apply between_equality with O; Between.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
           apply HDiff3; apply between_equality with O; eBetween|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet5 HBet6])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O B A) by eBetween.
            exfalso; apply HDiff5; apply between_equality with A; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H';
            elim HElim; clear HElim; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              elim (l5_3 O B BMA E); Between; intro HBet8; exfalso;
              [apply HDiff5; apply between_equality with BMA|
               apply HDiff8; apply between_equality with B]; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O B BMA) by eBetween.
              exfalso; apply HDiff5; apply between_equality with BMA; Between.
              }
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet O B A) by eBetween.
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet O B A) by eBetween.
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
           apply HDiff3; apply between_equality with O; eBetween|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet5 HBet6])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet A O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with A; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H';
            elim HElim; clear HElim; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet BMA O E) by eBetween.
              exfalso; apply HDiff8; apply between_equality with E; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet BMA O E) by eBetween.
              exfalso; apply HDiff1; apply between_equality with BMA; Between.
              }
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet B A C) by eBetween.
            exfalso; apply HDiff3; apply between_equality with C; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet B A C) by eBetween.
            exfalso; apply HDiff3; apply between_equality with C; Between.
            }
          }
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        exfalso; apply neg_not_pos in HNgB; apply HNgB; clear HNgB.
        do 2 (split; auto).
        destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
        elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
        [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
         apply HDiff3; apply between_equality with O; eBetween|].
        apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
        do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                   try destruct HBMA as [HBet3 HBet4])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet5 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet6;
          elim HElim2; clear HElim2; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet5 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet6;
          elim HElim2; clear HElim2; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet5; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet5; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }
        }
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      elim HColB; clear HColB; [intro HPsB|intro HNgB].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
        destruct HPsB as [H [H' HElim2]]; clear H; clear H'.
        elim HElim1; clear HElim1; intro HBet3;
        elim HElim2; clear HElim2; intro HBet4.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          elim (l5_3 O A B E); Between; intro HBet5.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            left; eBetween.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
            elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
            [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
             apply HDiff3; apply between_equality with O; Between|].
            apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
            do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                       try destruct HBMA as [HBet6 HBet7])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              exfalso; apply HDiff5; apply between_equality with A; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              destruct HPsBMA as [HDiff8 [H HElim]]; clear H.
              elim HElim; clear HElim; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
                {
                assert (HBet9 : Bet E O B)
                  by (apply outer_transitivity_between2 with BMA; Between).
                exfalso; apply HDiff5; apply between_equality with E; Between.
                }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
                {
                assert (HBet9 : Bet E O B) by eBetween.
                exfalso; apply HDiff5; apply between_equality with E; Between.
                }
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O A B)
                by (apply outer_transitivity_between2 with BMA; Between).
              exfalso; apply HDiff3; apply between_equality with O; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O A B) by eBetween.
              exfalso; apply HDiff3; apply between_equality with O; Between.
              }
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          elim (l5_3 O CMB E B); Between.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
           apply HDiff3; apply between_equality with O; eBetween|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet5 HBet6])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O B A) by eBetween.
            exfalso; apply HDiff5; apply between_equality with A; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H';
            elim HElim; clear HElim; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              elim (l5_3 O B BMA E); Between; intro HBet8; exfalso;
              [apply HDiff5; apply between_equality with BMA|
               apply HDiff8; apply between_equality with B]; Between.
              }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
              {
              assert (HBet8 : Bet O B BMA) by eBetween.
              exfalso; apply HDiff5; apply between_equality with BMA; Between.
              }
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet O B A) by eBetween.
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet7 : Bet O A B) by eBetween.
            assert (HBet8 : Bet O B A) by eBetween.
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          elim (l5_3 O CMB E B); Between.
          }
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        assert (HBet3 : Bet B O A).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H'' [H' H]]; unfold Ng in *; spliter;
          induction H; eBetween.
          }
        exfalso; apply neg_not_pos in HNgB; apply HNgB; clear HNgB.
        do 2 (split; auto).
        destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
        elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
        [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
         apply HDiff4; apply between_equality with B; eBetween|].
        apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
        do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                   try destruct HBMA as [HBet4 HBet5])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet6 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet7;
          elim HElim2; clear HElim2; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet6 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet7;
          elim HElim2; clear HElim2; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet6; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet6; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }
        }
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      elim HColB; clear HColB; [intro HPsB|intro HNgB].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HPsB as [H [H' HElim]]; clear H; clear H'.
        elim HElim; clear HElim; intro HBet3.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          elim (l5_2 O B CMB E); eBetween.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          right; eBetween.
          }
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        assert (HBet3 : Bet B O A).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H'' [H' H]]; unfold Ng in *; spliter;
          induction H; eBetween.
          }
        exfalso; apply neg_not_pos in HNgB; apply HNgB; clear HNgB.
        do 2 (split; auto).
        destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
        elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
        [apply l14_36_a in HBMA; try apply out_trivial; auto; exfalso;
         apply HDiff4; apply between_equality with B; eBetween|].
        apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
        do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                   try destruct HBMA as [HBet4 HBet5])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet6 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet7;
          elim HElim2; clear HElim2; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet6 : Bet BMA O A) by eBetween.
          destruct HPsA as [H [H' HElim1]]; clear H; clear H'.
          destruct HPsBMA as [HDiff8 [H' HElim2]]; clear H'.
          elim HElim1; clear HElim1; intro HBet7;
          elim HElim2; clear HElim2; intro HBet8.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff8; apply between_equality with E; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet9 : Bet BMA O E) by eBetween.
            exfalso; apply HDiff1; apply between_equality with BMA; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet6; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HPsA as [H [H' HElim]]; clear H; clear H'.
          elim HElim; clear HElim; intro HBet6; [|eBetween].
          elim (l5_2 O A B E); eBetween.
          }
        }
      }
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
    elim HColB; clear HColB; [intro HPsB|intro HNgB].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      do 3 (try (elim HCMB; clear HCMB; intro HCMB;
               try destruct HCMB as [HBet1 HBet2])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HNgA as [H [H' HBet3]]; clear H; clear H'.
        destruct HPsB as [H [H' HElim]]; clear H; clear H'.
        elim HElim; clear HElim; intro HBet4;
        assert (HBet5 : Bet O B C) by eBetween;
        exfalso; apply HDiff5; apply between_equality with C; Between.
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HNgA as [H [H' HBet3]]; clear H; clear H'.
        destruct HPsB as [H [H' HElim]]; clear H; clear H'.
        elim HElim; clear HElim; intro HBet4;
        assert (HBet5 : Bet O B C) by eBetween;
        exfalso; apply HDiff2; apply between_equality with O; Between.
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HPsB as [H [H' HElim]]; clear H; clear H'.
        elim HElim; clear HElim; intro HBet4; [left; eBetween|].
        elim (l5_3 O CMB E B); eBetween.
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HPsB as [H [H' HElim]]; clear H; clear H'.
        elim HElim; clear HElim; intro HBet4; [|right; eBetween].
        elim (l5_2 O B CMB E); eBetween.
        }
      }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
      {
      do 3 (try (elim HCMB; clear HCMB; intro HCMB;
               try destruct HCMB as [HBet1 HBet2])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HNgB as [H [H' HBet3]]; clear H; clear H'.
        elim (l5_2 B O C E); Between; [|right; eBetween]; intro HBet4.
        elim (l5_2 O C CMB E); eBetween.
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HNgB as [H [H' HBet3]]; clear H; clear H'.
        assert (HBet4 : Bet E O C) by eBetween.
        elim (l5_2 C O CMB E); Between.
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HNgA as [H [H' HBet3]]; clear H; clear H'.
        destruct HNgB as [H [H' HBet4]]; clear H; clear H'.
        elim (l5_2 E O A B); Between; intro HBet5.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [destruct HPsBMA as [H [H' HElim]]; clear H; clear H';
           elim HElim; clear HElim; intro HBet6; exfalso;
           [apply HDiff4; apply between_equality with E|
            apply HDiff1; apply between_equality with A]; Between|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet6 HBet7])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff4; apply between_equality with B; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet E O BMA) by eBetween.
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'.
            exfalso; elim HElim; clear HElim; intro HBet9;
            [apply HDiff8; apply between_equality with E|
             apply HDiff1; apply between_equality with BMA]; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet E O BMA) by eBetween.
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'.
            exfalso; elim HElim; clear HElim; intro HBet9;
            [apply HDiff8; apply between_equality with E|
             apply HDiff1; apply between_equality with BMA]; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet6 : Bet O B C).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            elim (eq_dec_points B CMB); intro HDiff7; treat_equalities; [|eBetween].
(* Goal: @eq (@Tpoint Tn) A B *)
            apply l14_36_a in HCMB'; try apply out_trivial; auto.
            }
          elim (l5_2 O B A C); Between; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff3; apply between_equality with C; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff2; apply between_equality with A; Between.
            }
          }
        }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
        {
        destruct HNgA as [H [H' HBet3]]; clear H; clear H'.
        destruct HNgB as [H [H' HBet4]]; clear H; clear H'.
        elim (l5_2 E O A B); Between; intro HBet5.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          destruct HLt as [BMA [HBMA HPsBMA]]; apply diff_sum in HBMA.
          elim (eq_dec_points A BMA); intro HDiff7; treat_equalities;
          [destruct HPsBMA as [H [H' HElim]]; clear H; clear H';
           elim HElim; clear HElim; intro HBet6; exfalso;
           [apply HDiff4; apply between_equality with E|
            apply HDiff1; apply between_equality with A]; Between|].
          apply sum_cong in HBMA; Col; apply plgf_bet in HBMA.
          do 3 (try (elim HBMA; clear HBMA; intro HBMA;
                     try destruct HBMA as [HBet6 HBet7])).

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff4; apply between_equality with B; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff3; apply between_equality with O; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet E O BMA) by eBetween.
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'.
            exfalso; elim HElim; clear HElim; intro HBet9;
            [apply HDiff8; apply between_equality with E|
             apply HDiff1; apply between_equality with BMA]; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            assert (HBet8 : Bet E O BMA) by eBetween.
            destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'.
            exfalso; elim HElim; clear HElim; intro HBet9;
            [apply HDiff8; apply between_equality with E|
             apply HDiff1; apply between_equality with BMA]; Between.
            }
          }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
          {
          assert (HBet6 : Bet O B C).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            elim (eq_dec_points B CMB); intro HDiff7; treat_equalities; [|eBetween].
(* Goal: @eq (@Tpoint Tn) A B *)
            apply l14_36_a in HCMB'; try apply out_trivial; auto.
            }

          elim (l5_2 O B A C); Between; intro HBet7.

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff3; apply between_equality with C; Between.
            }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
            {
            exfalso; apply HDiff2; apply between_equality with A; Between.
            }
          }
        }
      }
    }
  }
Qed.

Lemma bet_lt12_le13 : forall O E E' A B C,
  Bet A B C -> LtP O E E' A B -> LeP O E E' A C.
Proof.
(* Goal: forall (O E E' A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @LtP Tn O E E' B A), @LeP Tn O E E' C A *)
intros O E E' A B C HBet HLt.
(* Goal: @LeP Tn O E E' A C *)
apply leP_trans with B; [left; auto|].
(* Goal: @eq (@Tpoint Tn) A B *)
apply bet_lt12_le23 with A; auto.
Qed.

Lemma bet_lt21_le32 : forall O E E' A B C,
  Bet A B C -> LtP O E E' B A -> LeP O E E' C B.
Proof.
(* Goal: forall (O E E' A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @LtP Tn O E E' B A), @LeP Tn O E E' C A *)
intros O E E' A B C HBet HLt.
assert (HNC : ~ Col O E E')
  by (destruct HLt as [D [H H']]; apply diff_ar2 in H; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
elim (eq_dec_points B C); intro HDiff2; [right; auto|].
(* Goal: @LeP Tn O E E' C B *)
assert (HDiff3 : B <> A) by (apply ltP_neq with O E E'; auto).
assert (HColA : Col O E A)
  by (destruct HLt as [D [H H']]; apply diff_ar2 in H; unfold Ar2 in *; spliter; Col).
assert (HColB : Col O E B)
  by (destruct HLt as [D [H H']]; apply diff_ar2 in H; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
assert (HColC : Col O E C) by (assert_diffs; assert_cols; ColR).
(* Goal: @LeP Tn O E E' C B *)
destruct (diff_exists O E E' B C) as [BMC HBMC]; Col.
(* Goal: @LeP Tn O E E' C B *)
destruct (opp_exists O E E' HNC A) as [MA HMA]; Col.
(* Goal: @LeP Tn O E E' C B *)
destruct (opp_exists O E E' HNC B) as [MB HMB]; Col.
(* Goal: @LeP Tn O E E' AMC BMC *)
destruct (opp_exists O E E' HNC C) as [MC HMC]; Col.
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColMA : Col O E MA) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColMB : Col O E MB) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
assert (HColMC : Col O E MC) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
assert (HColBMC : Col O E BMC)
  by (apply diff_ar2 in HBMC; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
destruct (diff_exists O E E' A B) as [AMB HAMB]; Col.
assert (HColAMB : Col O E AMB)
  by (apply diff_ar2 in HAMB; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
destruct (diff_exists O E E' MA MB) as [MAMMB HMAMMB]; Col.
assert (HColMAMMB : Col O E MAMMB)
  by (apply diff_ar2 in HMAMMB; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
assert (HOppAMB : Opp O E E' AMB MAMMB).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  apply sum_opp; apply sum_assoc_1 with MB A B;
  [| |apply sum_comm; Col; apply diff_sum; apply diff_O_A; Col].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
(* Goal: @Sum Tn O E E' MB A AMB *)
    apply diff_sum in HAMB.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply sum_assoc_2 with B AMB O; auto.
(* Goal: @Sum Tn O E E' O BMC BMC *)
    apply sum_O_B; Col.
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
(* Goal: @Sum Tn O E E' A MAMMB B *)
    apply diff_sum in HMAMMB.
    apply sum_assoc_2 with MA B O; auto; try apply sum_O_B; Col;
    [apply diff_sum; apply diff_O_A; Col|].
(* Goal: @Sum Tn O E E' MA B MAMMB *)
    apply sum_assoc_1 with MAMMB MB O; auto; [apply sum_comm; auto|].
(* Goal: @Sum Tn O E E' MBMMC O MBMMC *)
    apply sum_A_O; Col.
    }
  }
(* Goal: @LeP Tn O E E' C B *)
destruct (diff_exists O E E' MB MA) as [MBMMA HMBMMA]; Col.
assert (HColMBMMA : Col O E MBMMA)
  by (apply diff_ar2 in HMBMMA; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
assert (HOppMAMMB : Opp O E E' MAMMB MBMMA) by (apply diff_opp with MA MB; auto).
assert (AMB = MBMMA)
  by (apply opp_uniqueness with O E E' MAMMB; auto; apply opp_comm; auto).
(* Goal: @LeP Tn O E E' C B *)
treat_equalities.
assert (HBet' : Bet MA MB MC)
  by (apply l7_15 with A B C O; auto; try apply opp_midpoint with E E'; auto).
(* Goal: @LeP Tn O E E' C B *)
destruct (diff_exists O E E' MB MC) as [MBMMC HMBMMC]; Col.
assert (HColMAMMC : Col O E MBMMC)
  by (apply diff_ar2 in HMBMMC; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' C B *)
assert (HOppAMC : Opp O E E' BMC MBMMC).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  apply sum_opp; apply sum_assoc_1 with MC B C;
  [| |apply sum_comm; Col; apply diff_sum; apply diff_O_A; Col].

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
(* Goal: @Sum Tn O E E' MC B BMC *)
    apply diff_sum in HBMC.
(* Goal: @eq (@Tpoint Tn) A B *)
    apply sum_assoc_2 with C BMC O; auto.
(* Goal: @Sum Tn O E E' O BMC BMC *)
    apply sum_O_B; Col.
    }

(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
    {
(* Goal: @Sum Tn O E E' B MBMMC C *)
    apply diff_sum in HMBMMC.
    apply sum_assoc_2 with MB C O; auto; try apply sum_O_B; Col;
    [apply diff_sum; apply diff_O_A; Col|].
(* Goal: @Sum Tn O E E' MB C MBMMC *)
    apply sum_assoc_1 with MBMMC MC O; auto; [apply sum_comm; auto|].
(* Goal: @Sum Tn O E E' MBMMC O MBMMC *)
    apply sum_A_O; Col.
    }
  }
(* Goal: @LeP Tn O E E' C B *)
destruct (diff_exists O E E' MC MB) as [MCMMB HMCMMB]; Col.
(* Goal: @LeP Tn O E E' C B *)
assert (HOppMBMMC : Opp O E E' MBMMC MCMMB) by (apply diff_opp with MB MC; auto).
assert (BMC = MCMMB)
  by (apply opp_uniqueness with O E E' MBMMC; auto; apply opp_comm; auto).
(* Goal: @LeP Tn O E E' C B *)
treat_equalities.
assert (HLt' : LtP O E E' MA MB)
  by (exists AMB; split; auto; apply lt_diff_ps with E' A B; auto).
(* Goal: @LeP Tn O E E' C B *)
assert (HLe : LeP O E E' MB MC) by (apply bet_lt12_le23 with MA; auto).
(* Goal: @eq (@Tpoint Tn) A B *)
left; exists BMC; split; auto; apply lt_diff_ps with E' MC MB; auto.
(* Goal: @LeP Tn O E E' C B *)
elim HLe; clear HLe; intro HFalse; auto; treat_equalities.
assert (O = BMC)
  by (apply diff_uniqueness with O E E' MB MB; auto; apply diff_null; Col).
(* Goal: not (and (not (@eq (@Tpoint Tn) O O)) (and (not (@eq (@Tpoint Tn) E O)) (or (@Bet Tn O O E) (@Bet Tn O E O)))) *)
treat_equalities; apply diff_null_eq in HBMC; treat_equalities; intuition.
Qed.

Lemma bet_lt21_le31 : forall O E E' A B C,
  Bet A B C -> LtP O E E' B A -> LeP O E E' C A.
Proof.
(* Goal: forall (O E E' A B C : @Tpoint Tn) (_ : @Bet Tn A B C) (_ : @LtP Tn O E E' B A), @LeP Tn O E E' C A *)
intros O E E' A B C HBet HLt.
(* Goal: @LeP Tn O E E' C A *)
apply leP_trans with B; [|left; auto].
(* Goal: @eq (@Tpoint Tn) A B *)
apply bet_lt21_le32 with A; auto.
Qed.

Lemma opp_2_le_le : forall O E E' A MA B MB,
  Opp O E E' A MA -> Opp O E E' B MB -> LeP O E E' A B -> LeP O E E' MB MA.
Proof.
(* Goal: forall (O E E' A MA B MB : @Tpoint Tn) (_ : @Opp Tn O E E' A MA) (_ : @Opp Tn O E E' B MB) (_ : @LeP Tn O E E' A B), @LeP Tn O E E' MB MA *)
intros O E E' A MA B MB HOppA HOppB HLe.
(* Goal: @LeP Tn O E E' MB MA *)
assert (HNC : ~ Col O E E') by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColA : Col O E A) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColMA : Col O E MA) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColB : Col O E B) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' MB MA *)
assert (HColMB : Col O E MB) by (unfold Opp, Sum, Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' MB MA *)
destruct (sum_exists O E E' HNC MA MB) as [MAMB HMAMB]; Col.
assert (HMA : Sum O E E' B MAMB MA)
  by (apply sum_assoc_2 with MB MA O; apply sum_comm; Col; apply sum_A_O; auto).
assert (HMB : Sum O E E' A MAMB MB)
  by (apply sum_assoc_2 with MA MB O; try apply sum_O_B; auto; apply sum_comm; auto).
(* Goal: @eq (@Tpoint Tn) A B *)
eapply compatibility_of_sum_with_order in HLe; [|apply HMB|apply HMA]; auto.
Qed.

Lemma diff_2_le_le : forall O E E' A B C AMC BMC,
  Diff O E E' A C AMC -> Diff O E E' B C BMC -> LeP O E E' A B ->
  LeP O E E' AMC BMC.
(* Goal: forall (O E E' A B C AMC BMC : @Tpoint Tn) (_ : @Diff Tn O E E' A C AMC) (_ : @Diff Tn O E E' B C BMC) (_ : @LeP Tn O E E' A B), @LeP Tn O E E' AMC BMC *)
intros O E E' A B C AMC BMC HAMC HBMC HLe.
assert (HNC : ~ Col O E E')
  by (apply diff_ar2 in HAMC; unfold Ar2 in *; spliter; Col).
assert (HColC : Col O E C)
  by (apply diff_ar2 in HAMC; unfold Ar2 in *; spliter; Col).
assert (HColAMC : Col O E AMC)
  by (apply diff_ar2 in HAMC; unfold Ar2 in *; spliter; Col).
assert (HColBMC : Col O E BMC)
  by (apply diff_ar2 in HBMC; unfold Ar2 in *; spliter; Col).
(* Goal: @LeP Tn O E E' AMC BMC *)
destruct (opp_exists O E E' HNC C) as [MC HMC]; Col.
(* Goal: @LeP Tn O E E' AMC BMC *)
assert (HAMC' : Sum O E E' A MC AMC).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  apply diff_sum in HAMC; apply sum_assoc_1 with AMC C O;
(* Goal: @Sum Tn O E E' O BMC BMC *)
  apply sum_comm; auto; apply sum_O_B; Col.
  }
(* Goal: @LeP Tn O E E' AMC BMC *)
assert (HBMC' : Sum O E E' B MC BMC).
(* Goal: @Sum Tn O E E' B MC BMC *)
(* Goal: @LeP Tn O E E' AMC BMC *)
  {
  apply diff_sum in HBMC; apply sum_assoc_1 with BMC C O;
(* Goal: @Sum Tn O E E' O BMC BMC *)
  apply sum_comm; auto; apply sum_O_B; Col.
  }
(* Goal: @eq (@Tpoint Tn) A B *)
apply compatibility_of_sum_with_order with A B MC; auto.
Qed.

End Order.
