proposition: Lemma characterization_of_betweenness_aux : forall O E E' S U1 U2 A AX AY B BX BY C CX CY BXMAX CXMAX AB AC IAC T, Cd O E S U1 U2 A AX AY -> Cd O E S U1 U2 B BX BY -> Cd O E S U1 U2 C CX CY -> ~ Col O E E' -> Col O E AX -> Col O E BX -> Col O E CX -> Col O E BXMAX -> Col O E CXMAX -> Col O E T -> Col O E AB -> Col O E AC -> Col O E IAC -> Diff O E E' BX AX BXMAX -> Diff O E E' CX AX CXMAX -> Length O E E' A B AB -> Length O E E' A C AC -> Prod O E E' T AC AB -> Prod O E E' IAC AC E -> Bet A B C -> A <> B -> A <> C -> B <> C -> Prod O E E' T CXMAX BXMAX.
proof: Proof. intros O E E' S U1 U2 A AX AY B BX BY C CX CY BXMAX CXMAX AB AC IAC T. intros HCdA HCdB HCdC HNC HColAX HColBX HColCX HColBXMAX HColCXMAX HColT. intros HColAB HColAC HColIAC HBXMAX HCXMAX HAB HAC HT HIAC HBet HDiff1 HDiff2 HDiff3. destruct (parallel_existence S U1 A) as [A1 [A2 [HDiff4 [HPar HCol]]]]; try (intro; unfold Cd, Cs in *; spliter; treat_equalities; intuition). assert (HAX' := HCdA). destruct HAX' as [H [H' [HAX' H'']]]; clear H; clear H'; clear H''. destruct HAX' as [AX' [HProjpAX' HCongAX']]. assert (HA : Projp AX' A A1 A2). { split; auto; induction (eq_dec_points A AX'); [treat_equalities; right|left; split]; Col. apply par_perp__perp with S U1; auto. destruct HProjpAX' as [Hclear HAX']; clear Hclear. induction HAX'; spliter; Perp; intuition. } assert (HBX' := HCdB). destruct HBX' as [H [H' [HBX' H'']]]; clear H; clear H'; clear H''. destruct HBX' as [BX' [HProjpBX' HCongBX']]. destruct (exists_projp A1 A2 BX') as [BX'' HBX'']; auto. assert (HCX' := HCdC). destruct HCX' as [H [H' [HCX' H'']]]; clear H; clear H'; clear H''. destruct HCX' as [CX' [HProjpCX' HCongCX']]. destruct (exists_projp A1 A2 CX') as [CX'' HCX'']; auto. elim (col_dec A B BX''); intro HABBX''. { elim (eq_dec_points A BX''); intro HABX''; treat_equalities. { assert (AX' = BX'). { elim (line_dec S U1 A1 A2); intro HLine. { assert (A = AX') by (apply col_projp_eq with S U1; auto; assert_diffs; spliter; ColR). treat_equalities; apply eq_sym; apply col_projp_eq with A1 A2; auto. assert (Col S U1 BX') by (apply projp_col with B; auto). assert_diffs; spliter; ColR. } { assert (HCol' : Col A AX' BX') by (apply projp2_col with A1 A2; auto). assert (HParS : Par_strict S U1 A1 A2); [|clear HLine]. { elim (col_dec S U1 A1); intro HCol''; [apply par_not_col_strict with A2|apply par_not_col_strict with A1]; Col ; try (intro; apply HLine); Col. } apply l6_21 with S U1 A AX'; Col; [| |apply l4_13 with O E AX|apply l4_13 with O E BX]; Col; intro; treat_equalities; apply HParS; exists A; split; Col; apply col_permutation_2; apply l4_13 with O E AX; Col. } } treat_equalities; assert (HPerp : Perp A C S U1). { assert (HCol' : Col AX' A B) by (apply projp2_col with S U1; auto). assert_cols; apply perp_sym; apply perp_col0 with A B; try apply projp_projp_perp with AX'; Col. } assert (AX' = CX') by (apply perp_projp2_eq with A C S U1; auto). treat_equalities; assert (AX = BX). { assert_diffs; apply col_cong_3_cong_3_eq with S U1 AX' O E; Cong. apply l4_13 with O E AX; auto. } assert (AX = CX). { assert_diffs; apply col_cong_3_cong_3_eq with S U1 AX' O E; Cong. apply l4_13 with O E AX; auto. } treat_equalities; assert (O = BXMAX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col); assert (O = CXMAX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col); treat_equalities; apply prod_0_r; unfold Prod, Ar2 in *; spliter; Col. } { assert (B = BX''). { apply col_par_projp2_eq with A1 A2 S U1 BX'; Par. assert (Col A1 A2 BX'') by (apply projp_col with BX'; auto); ColR. } assert (C = CX''). { apply col_par_projp2_eq with A1 A2 S U1 CX'; Par; assert_cols. assert (Col A1 A2 BX'') by (apply projp_col with BX'; auto); ColR. } treat_equalities. assert (HElim : LeP O E E' AX BX \/ LeP O E E' BX AX) by (apply col_2_le_or_ge; Col). elim HElim; clear HElim; intro HLe4. { destruct (length_existence O E E' B A) as [LAB HLAB]; Col. assert (LAXBX : Length O E E' BX AX LAB). { apply length_eq_cong_2 with B A; auto. assert (Cong AX BX AX' BX'). { apply cong_3_2_cong_4 with O E AX BX S U1 AX' BX' in HCongBX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A B AX' BX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with B]; auto. } apply cong_transitivity with AX' BX'; Cong. } assert (LAB = BXMAX) by (apply l16_9_1 with O E E' BX AX; Col; left; auto). elim HLe4; clear HLe4; intro HLt; treat_equalities; [|assert (AX' = BX') by (apply col_cong_3_cong_3_eq with O E AX S U1; try intro; treat_equalities; Col); treat_equalities; apply projp_id with AX' A B A1 A2 in HBX''; intuition]. apply bet_lt12_le13 with O E E' AX BX CX in HLt; [|apply bet_betCood_aux with O E S U1 U2 A AY B BY C CY; auto]. destruct (length_existence O E E' C A) as [LAC HLAC]; Col. assert (LAXCX : Length O E E' CX AX LAC). { apply length_eq_cong_2 with C A; auto. assert (Cong AX CX AX' CX'). { apply cong_3_2_cong_4 with O E AX CX S U1 AX' CX' in HCongCX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A C AX' CX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with C]; auto. } apply cong_transitivity with AX' CX'; Cong. } assert (LAC = CXMAX) by (apply l16_9_1 with O E E' CX AX; Col; left; auto). assert (AB = LAB). { apply length_uniqueness with O E E' A B; auto; apply length_eq_cong_2 with B A; Cong. } assert (AC = LAC); treat_equalities. { apply length_uniqueness with O E E' A C; auto; apply length_eq_cong_2 with C A; Cong. } auto. } { destruct (length_existence O E E' A B) as [LAB HLAB]; Col. assert (LAXBX : Length O E E' AX BX LAB). { apply length_eq_cong_2 with A B; auto. assert (Cong AX BX AX' BX'). { apply cong_3_2_cong_4 with O E AX BX S U1 AX' BX' in HCongBX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A B AX' BX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with B]; auto. } apply cong_transitivity with AX' BX'; Cong. } destruct (diff_exists O E E' AX BX) as [AXMBX HAXMBX]; Col. assert (LAB = AXMBX) by (apply l16_9_1 with O E E' AX BX; Col; left; auto). elim HLe4; clear HLe4; intro HLt; treat_equalities; [|assert (AX' = BX') by (apply col_cong_3_cong_3_eq with O E BX S U1; try intro; treat_equalities; Col); treat_equalities; apply projp_id with AX' A B A1 A2 in HBX''; intuition]. apply bet_lt21_le31 with O E E' AX BX CX in HLt; [|apply bet_betCood_aux with O E S U1 U2 A AY B BY C CY; auto]. destruct (length_existence O E E' A C) as [LAC HLAC]; Col. assert (LAXCX : Length O E E' AX CX LAC). { apply length_eq_cong_2 with A C; auto. assert (Cong AX CX AX' CX'). { apply cong_3_2_cong_4 with O E AX CX S U1 AX' CX' in HCongCX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A C AX' CX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with C]; auto. } apply cong_transitivity with AX' CX'; Cong. } destruct (diff_exists O E E' AX CX) as [AXMCX HAXMCX]; Col. assert (LAC = AXMCX) by (apply l16_9_1 with O E E' AX CX; Col; left; auto). treat_equalities. assert (Opp O E E' BXMAX LAB) by (apply diff_opp with BX AX; auto). assert (Opp O E E' CXMAX LAC) by (apply diff_opp with CX AX; auto). destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (AB = LAB) by (apply length_uniqueness with O E E' A B; auto). assert (AC = LAC) by (apply length_uniqueness with O E E' A C; auto). treat_equalities; apply prod_assoc2 with AC ME AB; [|apply opp_prod; auto; apply opp_comm| apply opp_prod; auto; apply opp_comm]; auto. } } } { destruct (length_existence O E E' A BX'') as [ABX'' HABX'']; Col. destruct (length_existence O E E' A CX'') as [ACX'' HACX'']; Col. assert (HColABX'' : Col O E ABX''). { destruct HABX'' as [H [H' [HElim H'']]]; clear H; clear H'; clear H''. elim HElim; clear HElim; intro HLt; treat_equalities; Col. destruct HLt as [D [HDiff H]]; clear H. apply diff_ar2 in HDiff; unfold Ar2 in *; spliter; Col. } assert (HColACX'' : Col O E ACX''). { destruct HACX'' as [H [H' [HElim H'']]]; clear H; clear H'; clear H''. elim HElim; clear HElim; intro HLt; treat_equalities; Col. destruct HLt as [D [HDiff H]]; clear H. apply diff_ar2 in HDiff; unfold Ar2 in *; spliter; Col. } destruct (prod_exists O E E' HNC AB ACX'') as [F HF]; Col. assert (HF' : Prodg O E E' ABX'' AC F). { apply thales with A B C BX'' CX'' AB ACX''; auto. { assert_diffs; auto. } { assert_cols; auto. } { apply projp_col in HBX''; apply projp_col in HCX''; ColR. } { destruct HBX'' as [H HElim1]; clear H; destruct HProjpBX' as [H HElim2]; clear H. destruct HCX'' as [H HElim3]; clear H; destruct HProjpCX' as [H HElim4]; clear H. elim HElim1; clear HElim1; intro H; destruct H as [HColBX'' HPerp1]; elim HElim2; clear HElim2; intro H; destruct H as [HColBX' HPerp2]; elim HElim3; clear HElim3; intro H; destruct H as [HColCX'' HPerp3]; elim HElim4; clear HElim4; intro H; destruct H as [HColCX' HPerp4]; treat_equalities. { assert (HCol1 : Par B BX' BX' BX'') by (apply par_perp2__par with S U1 A1 A2; Perp). elim HCol1; clear HCol1; intro HCol1; [exfalso; apply HCol1; exists BX'; Col|]. assert (HCol2 : Par C CX' CX' CX'') by (apply par_perp2__par with S U1 A1 A2; Perp). elim HCol2; clear HCol2; intro HCol2; [exfalso; apply HCol2; exists CX'; Col|]. left; apply l12_9_2D with A1 A2. { apply perp_sym; apply perp_col0 with BX' BX''; Perp; assert_diffs; spliter; Col. } { apply perp_sym; apply perp_col0 with CX' CX''; Perp; assert_diffs; spliter; Col. intro; treat_equalities; assert_cols; apply HABBX''; ColR. } } { assert (HCol1 : Par B BX' BX' BX'') by (apply par_perp2__par with S U1 A1 A2; Perp). elim HCol1; clear HCol1; intro HCol1; [exfalso; apply HCol1; exists BX'; Col|]. left; apply l12_9_2D with A1 A2; Perp. apply perp_sym; apply perp_col0 with BX' BX''; Perp; assert_diffs; spliter; Col. } { assert (HCol1 : Par B BX' BX' BX'') by (apply par_perp2__par with S U1 A1 A2; Perp). elim HCol1; clear HCol1; intro HCol1; [exfalso; apply HCol1; exists BX'; Col|]. left; apply l12_9_2D with A1 A2; Perp. apply perp_sym; apply perp_col0 with BX' BX''; Perp; assert_diffs; spliter; Col. apply perp_sym; apply par_perp__perp with S U1; Perp. } { right; auto. } { assert (HCol2 : Par C CX' CX' CX'') by (apply par_perp2__par with S U1 A1 A2; Perp). elim HCol2; clear HCol2; intro HCol2; [exfalso; apply HCol2; exists CX'; Col|]. left; apply l12_9_2D with A1 A2; Perp. apply perp_sym; apply perp_col0 with CX' CX''; Perp; assert_diffs; spliter; Col. intro; treat_equalities; assert_cols; apply HABBX''; ColR. } { left; apply l12_9_2D with A1 A2; Perp; Perp. } { left; apply l12_9_2D with A1 A2; Perp. apply perp_sym; apply par_perp__perp with S U1; Perp. } { right; auto. } { assert (HCol2 : Par C CX' CX' CX'') by (apply par_perp2__par with S U1 A1 A2; Perp). elim HCol2; clear HCol2; intro HCol2; [exfalso; apply HCol2; exists CX'; Col|]. left; apply l12_9_2D with A1 A2; Perp. { apply perp_sym; apply par_perp__perp with S U1; Perp. } { apply perp_sym; apply perp_col0 with CX' CX''; Perp; assert_diffs; spliter; Col. intro; treat_equalities; assert_cols; apply HABBX''; ColR. } } { left; apply l12_9_2D with A1 A2; Perp. apply perp_sym; apply par_perp__perp with S U1; Perp. } { left; apply l12_9_2D with A1 A2; Perp. apply perp_sym; apply par_perp__perp with S U1; Perp. apply perp_sym; apply par_perp__perp with S U1; Perp. } { right; auto. } { exfalso; apply HABBX''; Col. } { exfalso; apply HABBX''; Col. } { exfalso; apply HABBX''; Col. } { right; auto. } } { left; auto. } } elim HF'; clear HF'; intro HF'; [|destruct HF' as [HFalse H]; clear H; exfalso; apply HFalse; do 3 (split; Col)]. assert (HProd : Prod O E E' T ACX'' ABX''). { assert (HColF : Col O E F) by (unfold Prod, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC F IAC) as [G HG]; Col. assert (Prod O E E' ABX'' E G) by (apply prod_assoc2 with AC IAC F; auto; apply prod_comm; auto). assert (Prod O E E' ACX'' T G). { apply prod_assoc2 with AB IAC F; auto; apply prod_comm; auto. apply prod_assoc2 with AC T E; auto; apply prod_comm; auto. apply prod_1_r; Col. } assert (G = ABX'') by (apply prod_uniqueness with O E E' ABX'' E; auto; apply prod_1_r; Col). treat_equalities; apply prod_comm; auto. } assert (HElim : LeP O E E' AX BX \/ LeP O E E' BX AX) by (apply col_2_le_or_ge; Col). elim HElim; clear HElim; intro HLe4. { assert (LAXBX : Length O E E' BX AX ABX''). { apply length_eq_cong_2 with A BX''; auto. assert (Cong AX BX AX' BX'). { apply cong_3_2_cong_4 with O E AX BX S U1 AX' BX' in HCongBX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A BX'' AX' BX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with B]; auto. } apply cong_transitivity with AX' BX'; Cong. } assert (ABX'' = BXMAX) by (apply l16_9_1 with O E E' BX AX; Col; left; auto). elim HLe4; clear HLe4; intro HLt; treat_equalities; [|assert (AX' = BX') by (apply col_cong_3_cong_3_eq with O E AX S U1; try intro; treat_equalities; Col); treat_equalities; apply projp_id with AX' A BX'' A1 A2 in HBX''; auto; treat_equalities; exfalso; Col]. apply bet_lt12_le13 with O E E' AX BX CX in HLt; [|apply bet_betCood_aux with O E S U1 U2 A AY B BY C CY; auto]. assert (LAXCX : Length O E E' CX AX ACX''). { apply length_eq_cong_2 with A CX''; auto. assert (Cong AX CX AX' CX'). { apply cong_3_2_cong_4 with O E AX CX S U1 AX' CX' in HCongCX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A CX'' AX' CX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with C]; auto. } apply cong_transitivity with AX' CX'; Cong. } assert (ACX'' = CXMAX) by (apply l16_9_1 with O E E' CX AX; Col; left; auto). treat_equalities; auto. } { assert (LAXBX : Length O E E' AX BX ABX''). { apply length_eq_cong_2 with A BX''; auto. assert (Cong AX BX AX' BX'). { apply cong_3_2_cong_4 with O E AX BX S U1 AX' BX' in HCongBX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A BX'' AX' BX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with B]; auto. } apply cong_transitivity with AX' BX'; Cong. } destruct (diff_exists O E E' AX BX) as [AXMBX HAXMBX]; Col. assert (ABX'' = AXMBX) by (apply l16_9_1 with O E E' AX BX; Col; left; auto). elim HLe4; clear HLe4; intro HLt; treat_equalities; [|assert (AX' = BX') by (apply col_cong_3_cong_3_eq with O E BX S U1; try intro; treat_equalities; Col); treat_equalities; apply projp_id with AX' A BX'' A1 A2 in HBX''; auto; treat_equalities; exfalso; Col]. apply bet_lt21_le31 with O E E' AX BX CX in HLt; [|apply bet_betCood_aux with O E S U1 U2 A AY B BY C CY; auto]. assert (LAXCX : Length O E E' AX CX ACX''). { apply length_eq_cong_2 with A CX''; auto. assert (Cong AX CX AX' CX'). { apply cong_3_2_cong_4 with O E AX CX S U1 AX' CX' in HCongCX'; try intro; treat_equalities; Col; unfold Cong_4 in *; spliter; Cong. } assert (Cong A CX'' AX' CX'). { apply col_2_par_projp2_cong with S U1 A1 A2; auto; [apply projp_col with A|apply projp_col with C]; auto. } apply cong_transitivity with AX' CX'; Cong. } destruct (diff_exists O E E' AX CX) as [AXMCX HAXMCX]; Col. assert (ACX'' = AXMCX) by (apply l16_9_1 with O E E' AX CX; Col; left; auto). treat_equalities. assert (Opp O E E' BXMAX ABX'') by (apply diff_opp with BX AX; auto). assert (Opp O E E' CXMAX ACX'') by (apply diff_opp with CX AX; auto). destruct (opp_exists O E E' HNC E) as [ME HME]; Col. apply prod_assoc2 with ACX'' ME ABX''; [auto|apply opp_prod; auto; apply opp_comm; auto| apply opp_prod; auto; apply opp_comm; auto]. } } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths