proposition: 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: Proof. 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). assert (HDiff1 : O <> E) by (assert_diffs; auto). 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). assert (HColC : Col O E C) by 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| | |]. { destruct HLt as [B' [HB' HPs]]. assert (B = B') by (apply diff_uniqueness with O E E' B O; auto; apply diff_A_O; Col). 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])). { exfalso; apply HDiff3; apply between_equality with C; Between. } { exfalso; apply HDiff2; apply between_equality with O; Between. } { 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. } { 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. } } { apply ltP_neg in HLt; apply ps_le; Col. unfold Ng in *; spliter. elim (l5_2 A O C E); Between. } { rename CMB into MB. left; exists MB; split; auto; apply opp_neg_pos with E' 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]. { 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])). { apply HDiff2; apply between_equality with A; Between. } { 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. } { apply HDiff3; apply between_equality with O; Between. apply between_symmetry; apply outer_transitivity_between2 with BMA; auto. } { apply HDiff3; apply between_equality with O; Between. apply outer_transitivity_between2 with BMA; Between. } } { 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. } } { 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]. { do 3 (try (elim HCMB; clear HCMB; intro HCMB; try destruct HCMB as [HBet1 HBet2])). { elim HColB; clear HColB; [intro HPsB|intro HNgB]. { 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. { elim (l5_3 O A B E); Between; intro HBet5. { assert (HBet6 : Bet O B C) by eBetween. exfalso; apply HDiff5; apply between_equality with C; Between. } { 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])). { exfalso; apply HDiff5; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H HElim]]; clear H. elim HElim; clear HElim; intro HBet8. { assert (HBet9 : Bet E O B) by (apply outer_transitivity_between2 with BMA; Between). exfalso; apply HDiff5; apply between_equality with E; Between. } { assert (HBet9 : Bet E O B) by eBetween. exfalso; apply HDiff5; apply between_equality with E; Between. } } { assert (HBet8 : Bet O A B) by (apply outer_transitivity_between2 with BMA; Between). exfalso; apply HDiff3; apply between_equality with O; Between. } { assert (HBet8 : Bet O A B) by eBetween. exfalso; apply HDiff3; apply between_equality with O; Between. } } } { assert (HBet5 : Bet O B C) by eBetween. exfalso; apply HDiff5; apply between_equality with C; Between. } { 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])). { assert (HBet7 : Bet O B A) by eBetween. exfalso; apply HDiff5; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'; elim HElim; clear HElim; intro HBet7. { 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. } { assert (HBet8 : Bet O B BMA) by eBetween. exfalso; apply HDiff5; apply between_equality with BMA; Between. } } { 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. } { 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. } } { 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])). { assert (HBet7 : Bet A O E) by eBetween. exfalso; apply HDiff1; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'; elim HElim; clear HElim; intro HBet7. { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. } { 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. } } } { 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])). { 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. { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. } { 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. } } } { elim HColB; clear HColB; [intro HPsB|intro HNgB]. { 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. { elim (l5_3 O A B E); Between; intro HBet5. { assert (HBet6 : Bet O B C) by eBetween. exfalso; apply HDiff2; apply between_equality with O; Between. } { 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])). { exfalso; apply HDiff5; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H HElim]]; clear H. elim HElim; clear HElim; intro HBet8. { assert (HBet9 : Bet E O B) by (apply outer_transitivity_between2 with BMA; Between). exfalso; apply HDiff5; apply between_equality with E; Between. } { assert (HBet9 : Bet E O B) by eBetween. exfalso; apply HDiff5; apply between_equality with E; Between. } } { assert (HBet8 : Bet O A B) by (apply outer_transitivity_between2 with BMA; Between). exfalso; apply HDiff3; apply between_equality with O; Between. } { assert (HBet8 : Bet O A B) by eBetween. exfalso; apply HDiff3; apply between_equality with O; Between. } } } { assert (HBet5 : Bet O B C) by eBetween. exfalso; apply HDiff2; apply between_equality with O; Between. } { 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])). { assert (HBet7 : Bet O B A) by eBetween. exfalso; apply HDiff5; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'; elim HElim; clear HElim; intro HBet7. { 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. } { assert (HBet8 : Bet O B BMA) by eBetween. exfalso; apply HDiff5; apply between_equality with BMA; Between. } } { 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. } { 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. } } { 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])). { assert (HBet7 : Bet A O E) by eBetween. exfalso; apply HDiff1; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'; elim HElim; clear HElim; intro HBet7. { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. } { 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. } } } { 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])). { 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. { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet8 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. } { 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. } } } { elim HColB; clear HColB; [intro HPsB|intro HNgB]. { 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. { elim (l5_3 O A B E); Between; intro HBet5. { left; eBetween. } { 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])). { exfalso; apply HDiff5; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H HElim]]; clear H. elim HElim; clear HElim; intro HBet8. { assert (HBet9 : Bet E O B) by (apply outer_transitivity_between2 with BMA; Between). exfalso; apply HDiff5; apply between_equality with E; Between. } { assert (HBet9 : Bet E O B) by eBetween. exfalso; apply HDiff5; apply between_equality with E; Between. } } { assert (HBet8 : Bet O A B) by (apply outer_transitivity_between2 with BMA; Between). exfalso; apply HDiff3; apply between_equality with O; Between. } { assert (HBet8 : Bet O A B) by eBetween. exfalso; apply HDiff3; apply between_equality with O; Between. } } } { elim (l5_3 O CMB E B); Between. } { 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])). { assert (HBet7 : Bet O B A) by eBetween. exfalso; apply HDiff5; apply between_equality with A; Between. } { destruct HPsBMA as [HDiff8 [H' HElim]]; clear H'; elim HElim; clear HElim; intro HBet7. { 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. } { assert (HBet8 : Bet O B BMA) by eBetween. exfalso; apply HDiff5; apply between_equality with BMA; Between. } } { 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. } { 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. } } { elim (l5_3 O CMB E B); Between. } } { assert (HBet3 : Bet B O A). { 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])). { 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. { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. } { 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. } } } { elim HColB; clear HColB; [intro HPsB|intro HNgB]. { destruct HPsB as [H [H' HElim]]; clear H; clear H'. elim HElim; clear HElim; intro HBet3. { elim (l5_2 O B CMB E); eBetween. } { right; eBetween. } } { assert (HBet3 : Bet B O A). { 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])). { 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. { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff8; apply between_equality with E; Between. } { assert (HBet9 : Bet BMA O E) by eBetween. exfalso; apply HDiff1; apply between_equality with BMA; Between. } } { 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. } { 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. } } } } { elim HColB; clear HColB; [intro HPsB|intro HNgB]. { do 3 (try (elim HCMB; clear HCMB; intro HCMB; try destruct HCMB as [HBet1 HBet2])). { 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. } { 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. } { 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. } { 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. } } { do 3 (try (elim HCMB; clear HCMB; intro HCMB; try destruct HCMB as [HBet1 HBet2])). { 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. } { 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. } { 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. { 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])). { exfalso; apply HDiff4; apply between_equality with B; Between. } { exfalso; apply HDiff3; apply between_equality with O; Between. } { 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. } { 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. } } { assert (HBet6 : Bet O B C). { elim (eq_dec_points B CMB); intro HDiff7; treat_equalities; [|eBetween]. apply l14_36_a in HCMB'; try apply out_trivial; auto. } elim (l5_2 O B A C); Between; intro HBet7. { exfalso; apply HDiff3; apply between_equality with C; Between. } { exfalso; apply HDiff2; apply between_equality with A; Between. } } } { 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. { 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])). { exfalso; apply HDiff4; apply between_equality with B; Between. } { exfalso; apply HDiff3; apply between_equality with O; Between. } { 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. } { 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. } } { assert (HBet6 : Bet O B C). { elim (eq_dec_points B CMB); intro HDiff7; treat_equalities; [|eBetween]. apply l14_36_a in HCMB'; try apply out_trivial; auto. } elim (l5_2 O B A C); Between; intro HBet7. { exfalso; apply HDiff3; apply between_equality with C; Between. } { exfalso; apply HDiff2; apply between_equality with A; Between. } } } } } } Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod