proposition: 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: 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). elim (eq_dec_points B C); intro HDiff2; [right; auto|]. 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). assert (HColC : Col O E C) by ColR. destruct (diff_exists O E E' B C) as [BMC HBMC]; Col. destruct (opp_exists O E E' HNC A) as [MA HMA]; Col. destruct (opp_exists O E E' HNC B) as [MB HMB]; Col. destruct (opp_exists O E E' HNC C) as [MC HMC]; Col. assert (HColMA : Col O E MA) by (unfold Opp, Sum, Ar2 in *; spliter; Col). assert (HColMB : Col O E MB) by (unfold Opp, Sum, Ar2 in *; spliter; Col). 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). 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). 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). assert (HOppAMB : Opp O E E' AMB MAMMB). { apply sum_opp; apply sum_assoc_1 with MB A B; [| |apply sum_comm; Col; apply diff_sum; apply diff_O_A; Col]. { apply diff_sum in HAMB. apply sum_assoc_2 with B AMB O; auto. apply sum_O_B; Col. } { 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|]. apply sum_assoc_1 with MAMMB MB O; auto; [apply sum_comm; auto|]. apply sum_A_O; Col. } } 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). 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). 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). 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). assert (HOppAMC : Opp O E E' BMC MBMMC). { apply sum_opp; apply sum_assoc_1 with MC B C; [| |apply sum_comm; Col; apply diff_sum; apply diff_O_A; Col]. { apply diff_sum in HBMC. apply sum_assoc_2 with C BMC O; auto. apply sum_O_B; Col. } { 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|]. apply sum_assoc_1 with MBMMC MC O; auto; [apply sum_comm; auto|]. apply sum_A_O; Col. } } destruct (diff_exists O E E' MC MB) as [MCMMB HMCMMB]; Col. 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). treat_equalities. assert (HLt' : LtP O E E' MA MB) by (exists AMB; split; auto; apply lt_diff_ps with E' A B; auto). assert (HLe : LeP O E E' MB MC) by (apply bet_lt12_le23 with MA; auto). left; exists BMC; split; auto; apply lt_diff_ps with E' MC MB; auto. 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). treat_equalities; apply diff_null_eq in HBMC; treat_equalities; intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod