proposition: Lemma characterization_of_betweenness : forall O E E' S U1 U2 A AX AY B BX BY C CX CY BXMAX BYMAY CXMAX CYMAY, 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 -> Diff O E E' BX AX BXMAX -> Diff O E E' BY AY BYMAY -> Diff O E E' CX AX CXMAX -> Diff O E E' CY AY CYMAY -> (Bet A B C <-> exists T, O <> E /\ Col O E T /\ LeP O E E' O T /\ LeP O E E' T E /\ Prod O E E' T CXMAX BXMAX /\ Prod O E E' T CYMAY BYMAY).
proof: Proof. intros O E E' S U1 U2 A AX AY B BX BY C CX CY BXMAX BYMAY CXMAX CYMAY. intros HCdA HCdB HCdC HBXMAX HBYMAY HCXMAX HCYMAY. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HBXMAX; unfold Ar2 in *; spliter; Col). assert (HColAX : Col O E AX) by (apply diff_ar2 in HBXMAX; unfold Ar2 in *; spliter; Col). assert (HColAY : Col O E AY) by (apply diff_ar2 in HBYMAY; unfold Ar2 in *; spliter; Col). assert (HColBX : Col O E BX) by (apply diff_ar2 in HBXMAX; unfold Ar2 in *; spliter; Col). assert (HColBY : Col O E BY) by (apply diff_ar2 in HBYMAY; unfold Ar2 in *; spliter; Col). assert (HColCX : Col O E CX) by (apply diff_ar2 in HCXMAX; unfold Ar2 in *; spliter; Col). assert (HColCY : Col O E CY) by (apply diff_ar2 in HCYMAY; unfold Ar2 in *; spliter; Col). assert (HColBXMAX : Col O E BXMAX) by (apply diff_ar2 in HBXMAX; unfold Ar2 in *; spliter; Col). assert (HColBYMAY : Col O E BYMAY) by (apply diff_ar2 in HBYMAY; unfold Ar2 in *; spliter; Col). assert (HColCXMAX : Col O E CXMAX) by (apply diff_ar2 in HCXMAX; unfold Ar2 in *; spliter; Col). assert (HColCYMAY : Col O E CYMAY) by (apply diff_ar2 in HCYMAY; unfold Ar2 in *; spliter; Col). split; [intro HBet|intro HT]. { elim (eq_dec_points A B); intro HDiff1; treat_equalities. { assert (AX = BX /\ AY = BY) by (rewrite <- eq_points_coordinates; [|apply HCdA|apply HCdB]; auto). spliter; treat_equalities. assert (O = BXMAX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col). assert (O = BYMAY) by (apply diff_uniqueness with O E E' AY AY; auto; apply diff_null; Col). treat_equalities; exists O; split; try (intro; treat_equalities; Col). split; Col. split; try apply leP_refl. split; try apply ps_le; Between. split; apply prod_0_l; Col. } { elim (eq_dec_points A C); intro HDiff2; treat_equalities; [intuition|]. elim (eq_dec_points B C); intro HDiff3; treat_equalities. { assert (BX = CX /\ BY = CY) by (rewrite <- eq_points_coordinates; [|apply HCdB|apply HCdC]; auto). spliter; treat_equalities. assert (BXMAX = CXMAX) by (apply diff_uniqueness with O E E' BX AX; auto). assert (BYMAY = CYMAY) by (apply diff_uniqueness with O E E' BY AY; auto). treat_equalities; exists E; split; try (intro; treat_equalities; Col). split; Col. split; try apply ps_le; Between. split; try apply leP_refl. split; apply prod_1_l; Col. } { destruct (length_existence O E E' A B) as [AB HAB]; Col. destruct (length_existence O E E' A C) as [AC HAC]; Col. destruct (length_existence O E E' B C) as [BC HBC]; Col. assert (HSum : Sum O E E' AB BC AC) by (assert_diffs; apply triangular_equality_bis with A B C; auto). assert (HLe1 : LeP O E E' O AB) by (apply length_pos with A B; auto). assert (HLe2 : LeP O E E' AB AC) by (apply length_leP_le_2 with A B A C; try (apply l5_5_2; exists C); Cong). assert (HColAB : Col O E AB) by (unfold Length in *; spliter; Col). assert (HColAC : Col O E AC) by (unfold Length in *; spliter; Col). destruct (inv_exists O E E' AC) as [IAC HIAC]; Col; try (intro; unfold Length in *; spliter; treat_equalities; auto). assert (HColIAC : Col O E IAC) by (unfold Prod, Ar2 in *; spliter; Col). assert (HLe3 : LeP O E E' O IAC). { apply pos_inv_pos with AC; auto; try (intro; unfold Length in *; spliter; treat_equalities; auto). apply length_pos with A C; auto. } destruct (prod_exists O E E' HNC AB IAC) as [T HT]; Col. exists T; split; try (intro; treat_equalities; Col). split; [unfold Prod, Ar2 in *; spliter; Col|]. split; [apply compatibility_of_prod_with_order with AB IAC; auto|]. split; [apply le_pos_prod_le with AB AC IAC; auto; apply prod_comm; auto|]. assert (HColT : Col O E T) by (unfold Prod, Ar2 in *; spliter; Col). assert (HT' : Prod O E E' T AC AB) by (apply prod_assoc1 with AB IAC E; auto; apply prod_1_r; Col). split; [apply characterization_of_betweenness_aux with S U1 U2 A AX AY B BX BY C CX CY AB AC IAC| apply characterization_of_betweenness_aux with S U2 U1 A AY AX B BY BX C CY CX AB AC IAC ]; auto; apply coord_exchange_axes; auto. } } } { destruct HT as [T [H [HColT [HOLeT [HTLeE [HX HY]]]]]]; clear H. rename B into B'; rename BX into B'X; rename BY into B'Y; rename HCdB into HCdB'. rename BXMAX into B'XMAX; rename HBXMAX into HB'XMAX. rename BYMAY into B'YMAY; rename HBYMAY into HB'YMAY. rename HColBX into HColB'X; rename HColBY into HColB'Y. rename HColBXMAX into HColB'XMAX; rename HColBYMAY into HColB'YMAY. destruct (length_existence O E E' A C) as [AC HAC]; Col. assert (HColAC : Col O E AC) by (unfold Length in *; spliter; Col). assert (HLe1 : LeP O E E' O AC) by (apply length_pos with A C; auto). destruct (prod_exists O E E' HNC T AC) as [AB HT]; Col. assert (HColAB : Col O E AB) by (unfold Prod, Ar2 in *; spliter; Col). assert (HLe2 : LeP O E E' O AB) by (apply compatibility_of_prod_with_order with T AC; auto). assert (HB : exists B, Bet A B C /\ Length O E E' A B AB). { assert (Le O AB A C). { apply length_leP_le_1 with O E E' AB AC; auto. assert_diffs; repeat split; Cong. apply le_pos_prod_le with T E AC; auto; apply prod_1_l; Col. } destruct (le_bet A C O AB) as [B [HBet HCong]]; auto; exists B; split; auto. assert_diffs; repeat split; Cong. } destruct HB as [B [HBet HAB]]. elim (eq_dec_points A C); intro HDiff2; treat_equalities. { assert (AX = CX /\ AY = CY) by (rewrite <- eq_points_coordinates; [|apply HCdA|apply HCdC]; auto). spliter; treat_equalities. assert (O = CXMAX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col). assert (O = CYMAY) by (apply diff_uniqueness with O E E' AY AY; auto; apply diff_null; Col). treat_equalities. assert (O = B'XMAX) by (apply prod_uniqueness with O E E' T O; auto; apply prod_0_r; Col). assert (O = B'YMAY) by (apply prod_uniqueness with O E E' T O; auto; apply prod_0_r; Col). treat_equalities. assert (AX = B'X) by (apply diff_uniquenessA with O E E' AX O; auto). assert (AY = B'Y) by (apply diff_uniquenessA with O E E' AY O; auto). treat_equalities. assert (A = B') by (rewrite eq_points_coordinates; [|apply HCdA|apply HCdB']; auto). treat_equalities; Between. } { assert (HCdB : exists BX, exists BY, Cd O E S U1 U2 B BX BY) by (apply coordinates_of_point; unfold Cd in *; spliter; auto). destruct HCdB as [BX [BY HCdB]]. elim (eq_dec_points A B); intro HDiff1; treat_equalities; try (elim (eq_dec_points B C); intro HDiff3; treat_equalities). { assert (AX = BX /\ AY = BY) by (rewrite <- eq_points_coordinates; [|apply HCdA|apply HCdB]; auto). assert (O = AB); spliter; treat_equalities. { apply length_uniqueness with O E E' A A; auto; apply length_id_2; assert_diffs; auto. } elim (eq_dec_points O T); intro HOT; treat_equalities. { assert (O = B'XMAX) by (apply prod_uniqueness with O E E' O CXMAX; auto; apply prod_0_l; Col). assert (O = B'YMAY) by (apply prod_uniqueness with O E E' O CYMAY; auto; apply prod_0_l; Col). treat_equalities. assert (AX = B'X) by (apply diff_uniquenessA with O E E' AX O; auto; apply diff_null; Col). assert (AY = B'Y) by (apply diff_uniquenessA with O E E' AY O; auto; apply diff_null; Col). assert (A = B'); treat_equalities; Between. rewrite eq_points_coordinates; [|apply HCdA|apply HCdB']; auto. } { apply prod_null in HT; elim HT; clear HT; intro H; [intuition|]. apply eq_sym in H; treat_equalities; exfalso; apply HDiff2. apply length_id in HAC; spliter; auto. } } { assert (BX = CX /\ BY = CY) by (rewrite <- eq_points_coordinates; [|apply HCdB|apply HCdC]; auto). spliter; treat_equalities. assert (AB = AC) by (apply length_uniqueness with O E E' A B; auto). spliter; treat_equalities. assert (E = T); treat_equalities. { apply prod_uniquenessA with O E E' AB AB; try apply prod_1_l; auto. intro; treat_equalities; apply length_id in HAC; assert_diffs; induction HAC; auto. } assert (CXMAX = B'XMAX) by (apply prod_uniqueness with O E E' E CXMAX; auto; apply prod_1_l; Col). assert (CYMAY = B'YMAY) by (apply prod_uniqueness with O E E' E CYMAY; auto; apply prod_1_l; Col). treat_equalities. assert (BX = B'X) by (apply diff_uniquenessA with O E E' AX CXMAX; auto). assert (BY = B'Y) by (apply diff_uniquenessA with O E E' AY CYMAY; auto). assert (B = B'); treat_equalities; Between. rewrite eq_points_coordinates; [|apply HCdC|apply HCdB']; auto. } { destruct (inv_exists O E E' AC) as [IAC HIAC]; Col; try (intro; unfold Length in *; spliter; treat_equalities; auto). assert (HColIAC : Col O E IAC) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColBX : Col O E BX) by (apply Cd_Col in HCdB; spliter; Col). destruct (diff_exists O E E' BX AX) as [BXMAX HBXMAX]; Col. assert (HColBXMAX : Col O E BXMAX) by (apply diff_ar2 in HBXMAX; unfold Ar2 in *; spliter; Col). assert (HX' : Prod O E E' T CXMAX BXMAX). { apply characterization_of_betweenness_aux with S U1 U2 A AX AY B BX BY C CX CY AB AC IAC; auto. } assert (BXMAX = B'XMAX) by (apply prod_uniqueness with O E E' T CXMAX; auto). assert (HColBY : Col O E BY) by (apply Cd_Col in HCdB; spliter; Col). destruct (diff_exists O E E' BY AY) as [BYMAY HBYMAY]; Col. assert (HColBYMAY : Col O E BYMAY) by (apply diff_ar2 in HBYMAY; unfold Ar2 in *; spliter; Col). assert (HY' : Prod O E E' T CYMAY BYMAY). { apply characterization_of_betweenness_aux with S U2 U1 A AY AX B BY BX C CY CX AB AC IAC; auto; apply coord_exchange_axes; auto. } assert (BYMAY = B'YMAY) by (apply prod_uniqueness with O E E' T CYMAY; auto). treat_equalities. assert (BX = B'X) by (apply diff_uniquenessA with O E E' AX BXMAX; auto). assert (BY = B'Y) by (apply diff_uniquenessA with O E E' AY BYMAY; auto). treat_equalities. assert (B = B') by (rewrite eq_points_coordinates; [|apply HCdB|apply HCdB']; auto). treat_equalities; auto. } } } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths