proposition: Lemma characterization_of_collinearity : forall O E E' S U1 U2 A AX AY B BX BY C CX CY AXMBX AYMBY BXMCX BYMCY XProd YProd, 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' AX BX AXMBX -> Diff O E E' AY BY AYMBY -> Diff O E E' BX CX BXMCX -> Diff O E E' BY CY BYMCY -> Prod O E E' AXMBX BYMCY XProd -> Prod O E E' AYMBY BXMCX YProd -> (Col A B C <-> XProd = YProd).
proof: Proof. intros O E E' S U1 U2 A AX AY B BX BY C CX CY AXMBX AYMBY BXMCX BYMCY XProd YProd. intros HCdA HCdB HCdC HAXMBX HAYMBY HBXMCX HBYMCY HXProd HYProd. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HAXMBX; unfold Ar2 in *; spliter; Col). assert (HColAX : Col O E AX) by (apply diff_ar2 in HAXMBX; unfold Ar2 in *; spliter; Col). assert (HColAY : Col O E AY) by (apply diff_ar2 in HAYMBY; unfold Ar2 in *; spliter; Col). assert (HColBX : Col O E BX) by (apply diff_ar2 in HBXMCX; unfold Ar2 in *; spliter; Col). assert (HColBY : Col O E BY) by (apply diff_ar2 in HBYMCY; unfold Ar2 in *; spliter; Col). assert (HColCX : Col O E CX) by (apply diff_ar2 in HBXMCX; unfold Ar2 in *; spliter; Col). assert (HColCY : Col O E CY) by (apply diff_ar2 in HBYMCY; unfold Ar2 in *; spliter; Col). assert (HColAXMBX : Col O E AXMBX) by (apply diff_ar2 in HAXMBX; unfold Ar2 in *; spliter; Col). assert (HColAYMBY : Col O E AYMBY) by (apply diff_ar2 in HAYMBY; unfold Ar2 in *; spliter; Col). assert (HColBXMCX : Col O E BXMCX) by (apply diff_ar2 in HBXMCX; unfold Ar2 in *; spliter; Col). assert (HColBYMCY : Col O E BYMCY) by (apply diff_ar2 in HBYMCY; unfold Ar2 in *; 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). 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). destruct (diff_exists O E E' CX AX) as [CXMAX HCXMAX]; Col. assert (HColCXMAX : Col O E CXMAX) by (apply diff_ar2 in HCXMAX; unfold Ar2 in *; spliter; Col). destruct (diff_exists O E E' CY AY) as [CYMAY HCYMAY]; Col. assert (HColCYMAY : Col O E CYMAY) by (apply diff_ar2 in HCYMAY; unfold Ar2 in *; spliter; Col). destruct (diff_exists O E E' CX BX) as [CXMBX HCXMBX]; Col. assert (HColCXMBX : Col O E CXMBX) by (apply diff_ar2 in HCXMBX; unfold Ar2 in *; spliter; Col). destruct (diff_exists O E E' CY BY) as [CYMBY HCYMBY]; Col. assert (HColCYMBY : Col O E CYMBY) by (apply diff_ar2 in HCYMBY; unfold Ar2 in *; spliter; Col). destruct (diff_exists O E E' AX CX) as [AXMCX HAXMCX]; Col. assert (HColAXMCX : Col O E AXMCX) by (apply diff_ar2 in HAXMCX; unfold Ar2 in *; spliter; Col). destruct (diff_exists O E E' AY CY) as [AYMCY HAYMCY]; Col. assert (HColAYMCY : Col O E AYMCY) by (apply diff_ar2 in HAYMCY; unfold Ar2 in *; spliter; Col). assert (HColXProd : Col O E XProd) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColYProd : Col O E YProd) by (unfold Prod, Ar2 in *; spliter; Col). split; intro HCol; treat_equalities. { elim (eq_dec_points A B); intro HDiff1; elim (eq_dec_points A C); intro HDiff2; elim (eq_dec_points B C); intro HDiff3; treat_equalities; [|intuition|intuition| |intuition| | |]. { apply eq_points_coordinates with O E S U1 U2 B AX AY B BX BY in HCdA; auto. destruct HCdA as [H H']; clear H'; elim H; clear H; auto; intros; treat_equalities. assert (O = AXMBX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col). assert (O = AYMBY) by (apply diff_uniqueness with O E E' AY AY; auto; apply diff_null; Col). treat_equalities. assert (O = XProd) by (apply prod_uniqueness with O E E' O BYMCY; auto; apply prod_0_l; Col). assert (O = YProd) by (apply prod_uniqueness with O E E' O BXMCX; auto; apply prod_0_l; Col). treat_equalities; auto. } { apply eq_points_coordinates with O E S U1 U2 A AX AY A BX BY in HCdA; auto. destruct HCdA as [H H']; clear H'; elim H; clear H; auto; intros; treat_equalities. assert (O = AXMBX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col). assert (O = AYMBY) by (apply diff_uniqueness with O E E' AY AY; auto; apply diff_null; Col). treat_equalities. assert (O = XProd) by (apply prod_uniqueness with O E E' O BYMCY; auto; apply prod_0_l; Col). assert (O = YProd) by (apply prod_uniqueness with O E E' O BXMCX; auto; apply prod_0_l; Col). treat_equalities; auto. } { apply eq_points_coordinates with O E S U1 U2 A AX AY A CX CY in HCdC; auto. destruct HCdC as [H H']; clear H'; elim H; clear H; auto; intros; treat_equalities. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. apply prod_uniqueness with O E E' AXMBX BYMCY; auto. apply prod_assoc1 with BXMCX ME AYMBY; auto; [|apply prod_comm|apply prod_comm; auto]; apply opp_prod; auto; [apply diff_opp with BX AX|apply diff_opp with BY AY]; auto. } { apply eq_points_coordinates with O E S U1 U2 B BX BY B CX CY in HCdC; auto. destruct HCdC as [H H']; clear H'; elim H; clear H; auto; intros; treat_equalities. assert (O = BXMCX) by (apply diff_uniqueness with O E E' BX BX; auto; apply diff_null; Col). assert (O = BYMCY) by (apply diff_uniqueness with O E E' BY BY; auto; apply diff_null; Col). treat_equalities. assert (O = XProd) by (apply prod_uniqueness with O E E' AXMBX O; auto; apply prod_0_r; Col). assert (O = YProd) by (apply prod_uniqueness with O E E' AYMBY O; auto; apply prod_0_r; Col). treat_equalities; auto. } { destruct HCol as [HBet1|[HBet1|HBet1]]. { assert (HBet2 : Bet AX BX CX /\ Bet AY BY CY) by (apply bet_betCood with O E S U1 U2 A B C; auto). destruct HBet2 as [HBet2 HBet3]. assert (HBet':= HBet1). rewrite characterization_of_betweenness in HBet'; [|apply HCdA|apply HCdB|apply HCdC| apply HBXMAX|apply HBYMAY|apply HCXMAX| apply HCYMAY]. destruct HBet' as [T [HDiff4 [HColT [HLe1 [HLe2 [HProd1 HProd2]]]]]]. assert (HSumX : Sum O E E' AXMBX BXMCX AXMCX) by (apply sum_diff_diff with AX BX CX; auto). assert (HSumY : Sum O E E' AYMBY BYMCY AYMCY) by (apply sum_diff_diff with AY BY CY; auto). destruct (prod_exists O E E' HNC AXMBX AYMBY) as [P1 HP1]; Col. assert (HColP1 : Col O E P1) by (unfold Prod, Ar2 in *; spliter; Col). destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC ME T) as [P2 HP2]; Col. assert (HColP2 : Col O E P2) by (unfold Prod, Ar2 in *; spliter; Col). destruct (sum_exists O E E' HNC XProd P1) as [XProd' HXProd']; Col. assert (HColXProd' : Col O E XProd') by (unfold Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC AXMBX AYMCY) as [D HProdX']; Col. assert (XProd' = D); treat_equalities. { apply sum_uniqueness with O E E' XProd P1; auto. apply distr_l with AXMBX BYMCY AYMBY AYMCY; auto. apply sum_comm; auto. } destruct (sum_exists O E E' HNC YProd P1) as [YProd' HYProd']; Col. assert (HColYProd' : Col O E YProd') by (unfold Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC AYMBY AXMCX) as [D HProdY']; Col. assert (YProd' = D); treat_equalities. { apply sum_uniqueness with O E E' YProd P1; auto. apply distr_l with AYMBY BXMCX AXMBX AXMCX; auto; [apply sum_comm|apply prod_comm]; auto. } destruct (prod_exists O E E' HNC P2 XProd') as [XProd'' HXProd'']; Col. destruct (prod_exists O E E' HNC AXMBX BYMAY) as [D HProdX'']; Col. assert (XProd'' = D); treat_equalities. { apply prod_uniqueness with O E E' AXMBX BYMAY; auto. apply prod_assoc2 with AYMCY P2 XProd'; auto; apply prod_comm; auto. apply prod_assoc1 with T ME CYMAY; auto; apply prod_comm; auto. apply opp_prod; auto; apply diff_opp with AY CY; auto. } destruct (prod_exists O E E' HNC P2 YProd') as [YProd'' HYProd'']; Col. destruct (prod_exists O E E' HNC AYMBY BXMAX) as [D HProdY'']; Col. assert (YProd'' = D); treat_equalities. { apply prod_uniqueness with O E E' AYMBY BXMAX; auto. apply prod_assoc2 with AXMCX P2 YProd'; auto; apply prod_comm; auto. apply prod_assoc1 with T ME CXMAX; auto; apply prod_comm; auto. apply opp_prod; auto; apply diff_opp with AX CX; auto. } assert (XProd'' = YProd''); treat_equalities. { apply prod_uniqueness with O E E' AXMBX BYMAY; auto; apply prod_comm. apply prod_assoc1 with AYMBY ME BXMAX; auto; [|apply prod_comm]; apply opp_prod; auto; [apply diff_opp with AY BY|apply diff_opp with AX BX]; auto. } assert (XProd' = YProd'); treat_equalities. { apply prod_uniquenessB with O E E' P2 XProd''; auto. intro H; apply eq_sym in H; treat_equalities; apply prod_null in HP2. elim HP2; clear HP2; intro HFalse; apply eq_sym in HFalse; treat_equalities; [apply HDiff4; apply opp_uniqueness with O E E' O; try apply opp0; Col; apply opp_comm; auto|]. assert (O = BXMAX) by (apply prod_uniqueness with O E E' O CXMAX; auto; apply prod_0_l; Col). assert (O = BYMAY) by (apply prod_uniqueness with O E E' O CYMAY; auto; apply prod_0_l; Col). treat_equalities; apply diff_null_eq in HBXMAX; apply diff_null_eq in HBYMAY. treat_equalities; apply HDiff1; rewrite eq_points_coordinates; [|apply HCdA|apply HCdB]; auto. } apply sum_uniquenessA with O E E' P1 XProd'; auto. } { assert (HBet2 : Bet BX CX AX /\ Bet BY CY AY) by (apply bet_betCood with O E S U1 U2 B C A; auto). destruct HBet2 as [HBet2 HBet3]. assert (HBet':= HBet1). rewrite characterization_of_betweenness in HBet'; [|apply HCdB|apply HCdC|apply HCdA| apply HCXMBX|apply HCYMBY|apply HAXMBX| apply HAYMBY]. destruct HBet' as [T [HDiff4 [HColT [HLe1 [HLe2 [HProd1 HProd2]]]]]]. apply prod_uniqueness with O E E' AXMBX BYMCY; auto. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC ME T) as [P HP]; Col. apply prod_assoc2 with P AYMBY BXMCX; apply prod_comm; auto. { apply prod_assoc1 with ME T CXMBX; auto. apply prod_comm; apply opp_prod; auto. apply diff_opp with CX BX; auto. } { apply prod_assoc2 with T ME CYMBY; apply prod_comm; auto. apply prod_comm; apply opp_prod; auto. apply diff_opp with CY BY; auto. } } { assert (HBet2 : Bet CX AX BX /\ Bet CY AY BY) by (apply bet_betCood with O E S U1 U2 C A B; auto). destruct HBet2 as [HBet2 HBet3]. assert (HBet':= HBet1). rewrite characterization_of_betweenness in HBet'; [|apply HCdC|apply HCdA|apply HCdB| apply HAXMCX|apply HAYMCY|apply HBXMCX| apply HBYMCY]. destruct HBet' as [T [HDiff4 [HColT [HLe1 [HLe2 [HProd1 HProd2]]]]]]. assert (HSumX : Sum O E E' CXMAX AXMBX CXMBX) by (apply sum_diff_diff with CX AX BX; auto). assert (HSumY : Sum O E E' CYMAY AYMBY CYMBY) by (apply sum_diff_diff with CY AY BY; auto). destruct (prod_exists O E E' HNC CXMAX BYMCY) as [P1 HP1]; Col. destruct (prod_exists O E E' HNC CYMAY BXMCX) as [P2 HP1']; Col. assert (P1 = P2); treat_equalities. { apply prod_uniqueness with O E E' CXMAX BYMCY; auto. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC ME T) as [P HP]; Col. apply prod_assoc1 with BXMCX P CYMAY; apply prod_comm; auto. { apply prod_assoc1 with ME T AXMCX; auto. apply prod_comm; apply opp_prod; auto. apply diff_opp with AX CX; auto. } { apply prod_assoc2 with T ME AYMCY; apply prod_comm; auto. apply prod_comm; apply opp_prod; auto. apply diff_opp with AY CY; auto. } } assert (HColP1 : Col O E P1) by (unfold Prod, Ar2 in *; spliter; Col). destruct (sum_exists O E E' HNC XProd P1) as [XProd' HXProd']; Col. destruct (prod_exists O E E' HNC CXMBX BYMCY) as [P2 HP2]; Col. assert (P2 = XProd'); treat_equalities. { apply sum_uniqueness with O E E' XProd P1; auto. apply sum_comm; Col. apply distr_r with CXMAX AXMBX BYMCY CXMBX; auto. } destruct (sum_exists O E E' HNC YProd P1) as [YProd' HYProd']; Col. assert (P2 = YProd'); treat_equalities. { apply sum_uniqueness with O E E' YProd P1; auto. apply sum_comm; Col. apply distr_r with CYMAY AYMBY BXMCX CYMBY; auto. apply prod_comm; auto. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). apply prod_assoc1 with CXMBX ME BYMCY; auto. { apply opp_prod; auto. apply diff_opp with CX BX; auto. } { apply prod_comm; apply opp_prod; auto. apply diff_opp with CY BY; auto. } } apply sum_uniquenessA with O E E' P1 P2; auto. } } } { elim (eq_dec_points O AXMBX); intro HDiff1; treat_equalities; try apply diff_null_eq in HAXMBX; elim (eq_dec_points O AYMBY); intro HDiff2; treat_equalities; try apply diff_null_eq in HAYMBY; elim (eq_dec_points O BXMCX); intro HDiff3; treat_equalities; try apply diff_null_eq in HBXMCX; elim (eq_dec_points O BYMCY); intro HDiff4; treat_equalities; try apply diff_null_eq in HBYMCY; treat_equalities. { assert (A = B) by (rewrite eq_points_coordinates; [|apply HCdA|apply HCdB]; auto). treat_equalities; Col. } { assert (A = B) by (rewrite eq_points_coordinates; [|apply HCdA|apply HCdB]; auto). treat_equalities; Col. } { assert (A = B) by (rewrite eq_points_coordinates; [|apply HCdA|apply HCdB]; auto). treat_equalities; Col. } { assert (A = B) by (rewrite eq_points_coordinates; [|apply HCdA|apply HCdB]; auto). treat_equalities; Col. } { assert (B = C) by (rewrite eq_points_coordinates; [|apply HCdB|apply HCdC]; auto). treat_equalities; Col. } { apply same_abscissa_col with O E S U1 U2 AX AY BY CY; auto. } { apply prod_O_l_eq in HXProd; apply eq_sym in HXProd; treat_equalities. apply prod_null in HYProd; elim HYProd; clear HYProd; intro H; apply eq_sym in H; treat_equalities; intuition. } { apply prod_O_l_eq in HXProd; apply eq_sym in HXProd; treat_equalities. apply prod_null in HYProd; elim HYProd; clear HYProd; intro H; apply eq_sym in H; treat_equalities; intuition. } { assert (B = C) by (rewrite eq_points_coordinates; [|apply HCdB|apply HCdC]; auto). treat_equalities; Col. } { apply prod_O_l_eq in HYProd; apply eq_sym in HYProd; treat_equalities. apply prod_null in HXProd; elim HXProd; clear HXProd; intro H; apply eq_sym in H; treat_equalities; intuition. } { apply same_abscissa_col with O E S U2 U1 AY AX BX CX; auto; apply coord_exchange_axes; auto. } { apply prod_O_l_eq in HYProd; apply eq_sym in HYProd; treat_equalities. apply prod_null in HXProd; elim HXProd; clear HXProd; intro H; apply eq_sym in H; treat_equalities; intuition. } { assert (B = C) by (rewrite eq_points_coordinates; [|apply HCdB|apply HCdC]; auto). treat_equalities; Col. } { apply prod_O_r_eq in HYProd; apply eq_sym in HYProd; treat_equalities. apply prod_null in HXProd; elim HXProd; clear HXProd; intro H; apply eq_sym in H; treat_equalities; intuition. } { apply prod_O_r_eq in HXProd; apply eq_sym in HXProd; treat_equalities. apply prod_null in HYProd; elim HYProd; clear HYProd; intro H; apply eq_sym in H; treat_equalities; intuition. } { destruct (length_existence O E E' AX BX) as [L1 HL1]; Col. assert (HColL1 : Col O E L1) by (unfold Length in *; spliter; Col). destruct (length_existence O E E' AX CX) as [L2 HL2]; Col. assert (HColL2 : Col O E L2) by (unfold Length in *; spliter; Col). destruct (length_existence O E E' BX CX) as [L3 HL3]; Col. assert (HColL3 : Col O E L3) by (unfold Length in *; spliter; Col). assert (HElim : LeP O E E' L1 L3 /\ LeP O E E' L2 L3 \/ LeP O E E' L1 L2 /\ LeP O E E' L3 L2 \/ LeP O E E' L2 L1 /\ LeP O E E' L3 L1). { assert (H1 : LeP O E E' L1 L2 \/ LeP O E E' L2 L1) by (apply col_2_le_or_ge; Col). assert (H2 : LeP O E E' L1 L3 \/ LeP O E E' L3 L1) by (apply col_2_le_or_ge; Col). assert (H3 : LeP O E E' L2 L3 \/ LeP O E E' L3 L2) by (apply col_2_le_or_ge; Col). elim H1; clear H1; intro HLe1; elim H2; clear H2; intro HLe2; elim H3; clear H3; intro HLe3; auto. { left; split; [apply leP_trans with L2|]; assumption. } { left; split; [|apply leP_trans with L1]; assumption. } } destruct HElim as [Hc|[Hc|Hc]]; destruct Hc as [HLe1 HLe2]; [right; right|left|right; left]. { assert (HBetX : Bet CX AX BX). { apply l5_12_b; [ColR| apply length_leP_le_1 with O E E' L2 L3| apply length_leP_le_1 with O E E' L1 L3]; auto; apply length_sym; auto. } rewrite characterization_of_betweenness; [|apply HCdC|apply HCdA|apply HCdB| apply HAXMCX|apply HAYMCY|apply HBXMCX|apply HBYMCY]. assert (HDiff5 : O <> L3). { intro; treat_equalities; apply length_id in HL3; spliter; treat_equalities. apply HDiff1; apply diff_uniqueness with O E E' BX BX; auto; apply diff_null; Col. } assert (HLe3 : LeP O E E' O L3) by (apply length_pos with BX CX; auto). destruct (inv_exists O E E' L3) as [IBC HIBC]; Col. assert (HColIBC : Col O E IBC) by (unfold Prod, Ar2 in *; spliter; Col). assert (HLe4 : LeP O E E' O IBC) by (apply pos_inv_pos with L3; auto). destruct (prod_exists O E E' HNC L2 IBC) as [T HT]; Col; exists T. split; try (intro; treat_equalities; Col). split; [unfold Prod, Ar2 in *; spliter; Col|]. assert (HLe5 : LeP O E E' O L2) by (apply length_pos with AX CX; auto). split; [apply compatibility_of_prod_with_order with L2 IBC; auto|]. split; [apply le_pos_prod_le with L2 L3 IBC; auto; apply prod_comm; auto|]. assert (HDiff6 : O <> E) by (assert_diffs; auto). destruct (prod_exists O E E' HNC BXMCX BYMCY) as [P HP]; Col. destruct (prod_exists O E E' HNC AXMCX BYMCY) as [Pr HProd1]; Col. assert (HSum : Sum O E E' XProd P Pr). { apply distr_l with BYMCY AXMBX BXMCX AXMCX; auto; try apply prod_comm; auto. apply sum_diff_diff with AX BX CX; auto. } assert (HProd2 : Prod O E E' AYMCY BXMCX Pr). { destruct (prod_exists O E E' HNC AYMCY BXMCX) as [P' HP']; Col. assert (Pr = P'); treat_equalities; auto. apply sum_uniqueness with O E E' XProd P; auto. apply distr_l with BXMCX AYMBY BYMCY AYMCY; auto; try apply prod_comm; auto. apply sum_diff_diff with AY BY CY; auto. } assert (HProd3 : Prod O E E' T L3 L2). { apply prod_assoc1 with L2 IBC E; auto; try apply prod_1_r; Col. } elim (eq_dec_points O L2); intro HDiff7; treat_equalities. { assert (O = T) by (apply prod_uniqueness with O E E' O IBC; auto; apply prod_0_l; Col). apply length_id in HL2; spliter; treat_equalities. assert (O = AXMCX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col). treat_equalities; split; [apply prod_0_l; Col|]. apply diff_null_eq in HAXMCX; treat_equalities. assert (BXMAX = BXMCX) by (apply diff_uniqueness with O E E' BX AX; auto). treat_equalities. assert (AYMBY = CYMBY). { apply prod_uniquenessA with O E E' BXMAX XProd; auto; apply prod_comm. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. apply prod_assoc1 with AXMBX ME BYMCY; auto; [apply diff_2_prod with AX BX| apply prod_comm; apply diff_2_prod with CY BY]; auto. } assert (AY = CY); treat_equalities. { apply diff_uniquenessA with O E E' BY AYMBY; auto. } assert (O = AYMCY); treat_equalities; [|apply prod_0_l; Col]. apply diff_uniqueness with O E E' AY AY; auto. apply diff_null; Col. } { elim (length_eq_or_opp O E E' AX CX L2 AXMCX); auto; try apply length_sym; auto; intro HOpp; treat_equalities. { assert (HLe6 : LtP O E E' CX AX). { assert (H : LeP O E E' CX AX). { apply compatibility_of_sum_with_order with O L2 CX; auto; try apply sum_O_B; Col; apply sum_comm; Col; apply diff_sum; auto. } elim H; clear H; intro H; auto; treat_equalities. exfalso; apply HDiff7; apply diff_uniqueness with O E E' CX CX; auto. apply diff_null; Col. } assert (HLe7 : LeP O E E' CX BX) by (apply bet_lt12_le13 with AX; auto). assert (L3 = BXMCX) by (apply l16_9_1 with O E E' BX CX; auto; left; auto). treat_equalities; split; auto. apply prod_assoc1 with IBC L2 Pr; auto; apply prod_comm; auto. apply prod_assoc1 with AYMCY L3 E; auto; apply prod_comm; auto. apply prod_1_l; Col. } { assert (L2 = CXMAX); treat_equalities. { apply opp_uniqueness with O E E' AXMCX; Col; apply opp_comm; auto. apply diff_opp with CX AX; auto. } assert (HLe6 : LtP O E E' AX CX). { assert (H : LeP O E E' AX CX). { apply compatibility_of_sum_with_order with O L2 AX; auto; try apply sum_O_B; Col; apply sum_comm; Col; apply diff_sum; auto. } elim H; clear H; intro H; auto; treat_equalities. exfalso; apply HDiff7; apply diff_uniqueness with O E E' AX AX; auto. apply diff_null; Col. } assert (HLe7 : LeP O E E' BX CX) by (apply bet_lt21_le31 with AX; auto). assert (L3 = CXMBX); treat_equalities. { apply l16_9_1 with O E E' CX BX; auto; left; auto; apply length_sym; auto. } destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColT : Col O E T) by (unfold Prod, Ar2 in *; spliter; Col). assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). destruct (prod_exists O E E' HNC ME T) as [OppT HMT]; Col. assert (Prod O E E' T BXMCX AXMCX); [|split; auto]. { apply prod_assoc2 with ME L3 OppT; apply prod_comm; auto; [apply opp_prod; auto; apply diff_opp with CX BX; auto| apply prod_assoc2 with T ME L2; apply prod_comm; auto; apply prod_comm; apply opp_prod; auto]. } destruct (opp_exists O E E' HNC IBC) as [MIBC HMIBC]; Col. apply prod_assoc1 with MIBC AXMCX Pr; auto; apply prod_comm; auto. { apply prod_assoc2 with ME IBC L2; auto; [|apply prod_comm]; apply opp_prod; auto; apply diff_opp with AX CX; auto. } { destruct (opp_exists O E E' HNC Pr) as [MProd HMProd]; Col; [unfold Prod, Ar2 in *; spliter; Col|]. apply prod_assoc2 with ME IBC MProd; auto; [apply opp_prod|apply prod_comm; apply opp_prod|]; auto. apply prod_assoc1 with AYMCY L3 E; auto; apply prod_comm; auto; try apply prod_1_l; Col. apply prod_assoc1 with ME BXMCX Pr; apply prod_comm; auto; apply opp_prod; auto; apply diff_opp with BX CX; auto. } } } } { assert (HBetX : Bet AX BX CX). { apply l5_12_b; [ColR| apply length_leP_le_1 with O E E' L1 L2| apply length_leP_le_1 with O E E' L3 L2]; auto; apply length_sym; auto. } rewrite characterization_of_betweenness; [|apply HCdA|apply HCdB|apply HCdC| apply HBXMAX|apply HBYMAY|apply HCXMAX|apply HCYMAY]. assert (HDiff5 : O <> L2). { intro; treat_equalities; apply length_id in HL2; spliter; treat_equalities. apply HDiff1; apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col. } assert (HLe3 : LeP O E E' O L2) by (apply length_pos with AX CX; auto). destruct (inv_exists O E E' L2) as [IAC HIAC]; Col. assert (HColIAC : Col O E IAC) by (unfold Prod, Ar2 in *; spliter; Col). assert (HLe4 : LeP O E E' O IAC) by (apply pos_inv_pos with L2; auto). destruct (prod_exists O E E' HNC L1 IAC) as [T HT]; Col; exists T. split; try (intro; treat_equalities; Col). split; [unfold Prod, Ar2 in *; spliter; Col|]. assert (HLe5 : LeP O E E' O L1) by (apply length_pos with AX BX; auto). split; [apply compatibility_of_prod_with_order with L1 IAC; auto|]. split; [apply le_pos_prod_le with L1 L2 IAC; auto; apply prod_comm; auto|]. assert (HDiff6 : O <> E) by (assert_diffs; auto). destruct (prod_exists O E E' HNC AXMBX AYMBY) as [P HP]; Col. destruct (prod_exists O E E' HNC AXMCX AYMBY) as [Pr HProd1]; Col. assert (HSum : Sum O E E' XProd P Pr). { apply distr_l with AYMBY BXMCX AXMBX AXMCX; auto; try apply prod_comm; auto. apply sum_comm; Col; apply sum_diff_diff with AX BX CX; auto. } assert (HProd2 : Prod O E E' AYMCY AXMBX Pr). { destruct (prod_exists O E E' HNC AYMCY AXMBX) as [P' HP']; Col. assert (Pr = P'); treat_equalities; auto. apply sum_uniqueness with O E E' XProd P; auto. apply distr_l with AXMBX BYMCY AYMBY AYMCY; auto; try apply prod_comm; auto. apply sum_comm; Col; apply sum_diff_diff with AY BY CY; auto. } assert (HProd3 : Prod O E E' T L2 L1). { apply prod_assoc1 with L1 IAC E; auto; try apply prod_1_r; Col. } elim (eq_dec_points O L1); intro HDiff7; treat_equalities. { apply length_id in HL1; spliter; treat_equalities. assert (O = AXMBX) by (apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col). treat_equalities; intuition. } { elim (length_eq_or_opp O E E' AX BX L1 AXMBX); auto; try apply length_sym; auto; intro HOpp; treat_equalities. { assert (HLe6 : LtP O E E' BX AX). { assert (H : LeP O E E' BX AX). { apply compatibility_of_sum_with_order with O L1 BX; auto; try apply sum_O_B; Col; apply sum_comm; Col; apply diff_sum; auto. } elim H; clear H; intro H; auto; treat_equalities. exfalso; apply HDiff1; apply diff_uniqueness with O E E' BX BX; auto. apply diff_null; Col. } assert (HLe7 : LeP O E E' CX AX) by (apply bet_lt21_le31 with BX; auto). assert (L2 = AXMCX) by (apply l16_9_1 with O E E' AX CX; auto; left; auto). treat_equalities. assert (HProd4 : Prod O E E' T CXMAX BXMAX); [|split; auto]. { destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). apply prod_assoc1 with L1 IAC ME; auto; [|apply opp_prod; auto; apply diff_opp with AX BX; auto]. apply prod_assoc2 with L2 ME E; auto; apply opp_prod; auto. apply diff_opp with AX CX; auto. } destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColProd : Col O E Pr) by (unfold Prod, Ar2 in *; spliter; Col). destruct (opp_exists O E E' HNC Pr) as [MProd HMProd]; Col. apply prod_assoc1 with IAC L1 MProd; auto; apply prod_comm; auto; [apply prod_assoc1 with ME AYMCY Pr; auto; apply prod_comm; apply opp_prod; auto; apply diff_opp with AY CY; auto|]. apply prod_assoc1 with BYMAY L2 E; apply prod_comm; auto; try apply prod_1_l; Col; apply prod_assoc2 with AYMBY ME Pr; auto; apply opp_prod; auto; apply diff_opp with AY BY; auto. } { assert (L1 = BXMAX); treat_equalities. { apply opp_uniqueness with O E E' AXMBX; Col; apply opp_comm; auto. apply diff_opp with BX AX; auto. } assert (HLe6 : LtP O E E' AX BX). { assert (H : LeP O E E' AX BX). { apply compatibility_of_sum_with_order with O L1 AX; auto; try apply sum_O_B; Col; apply sum_comm; Col; apply diff_sum; auto. } elim H; clear H; intro H; auto; treat_equalities. exfalso; apply HDiff7; apply diff_uniqueness with O E E' AX AX; auto. apply diff_null; Col. } assert (HLe7 : LeP O E E' AX CX) by (apply bet_lt12_le13 with BX; auto). assert (L2 = CXMAX); treat_equalities. { apply l16_9_1 with O E E' CX AX; auto; left; apply length_sym; auto. } split; auto. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. apply prod_assoc1 with IAC L1 Pr; apply prod_comm; auto; [apply prod_assoc1 with AYMCY ME AXMBX; auto; [|apply prod_comm]; apply opp_prod; auto; apply diff_opp with AY CY; auto|]. apply prod_assoc1 with BYMAY L2 E; apply prod_comm; auto; try apply prod_1_l; Col. apply prod_assoc1 with AXMCX ME AYMBY; auto; [|apply prod_comm]; apply opp_prod; auto; [apply diff_opp with AX CX|apply diff_opp with BY AY]; auto. } } } { assert (HBetX : Bet BX CX AX). { apply l5_12_b; [ColR| apply length_leP_le_1 with O E E' L3 L1| apply length_leP_le_1 with O E E' L2 L1]; auto; apply length_sym; auto. } rewrite characterization_of_betweenness; [|apply HCdB|apply HCdC|apply HCdA| apply HCXMBX|apply HCYMBY|apply HAXMBX|apply HAYMBY]. assert (HDiff5 : O <> L1). { intro; treat_equalities; apply length_id in HL1; spliter; treat_equalities. apply HDiff1; apply diff_uniqueness with O E E' AX AX; auto; apply diff_null; Col. } assert (HLe3 : LeP O E E' O L1) by (apply length_pos with AX BX; auto). destruct (inv_exists O E E' L1) as [IAB HIAB]; Col. assert (HColIAB : Col O E IAB) by (unfold Prod, Ar2 in *; spliter; Col). assert (HLe4 : LeP O E E' O IAB) by (apply pos_inv_pos with L1; auto). destruct (prod_exists O E E' HNC L3 IAB) as [T HT]; Col; exists T. split; try (intro; treat_equalities; Col). split; [unfold Prod, Ar2 in *; spliter; Col|]. assert (HLe5 : LeP O E E' O L3) by (apply length_pos with BX CX; auto). split; [apply compatibility_of_prod_with_order with L3 IAB; auto|]. split; [apply le_pos_prod_le with L3 L1 IAB; auto; apply prod_comm; auto|]. assert (HDiff6 : O <> E) by (assert_diffs; auto). assert (HProd1 : Prod O E E' T L1 L3). { apply prod_assoc1 with L3 IAB E; auto; try apply prod_1_r; Col. } elim (eq_dec_points O L3); intro HDiff7; treat_equalities. { apply length_id in HL3; spliter; treat_equalities. assert (O = BXMCX) by (apply diff_uniqueness with O E E' BX BX; auto; apply diff_null; Col). treat_equalities; intuition. } { elim (length_eq_or_opp O E E' BX CX L3 BXMCX); auto; try apply length_sym; auto; intro HOpp; treat_equalities. { assert (HLe6 : LtP O E E' CX BX). { assert (H : LeP O E E' CX BX). { apply compatibility_of_sum_with_order with O L3 CX; auto; try apply sum_O_B; Col; apply sum_comm; Col; apply diff_sum; auto. } elim H; clear H; intro H; auto; treat_equalities. exfalso; apply HDiff3; apply diff_uniqueness with O E E' CX CX; auto. apply diff_null; Col. } assert (HLe7 : LeP O E E' AX BX) by (apply bet_lt21_le31 with CX; auto). assert (L1 = BXMAX) by (apply l16_9_1 with O E E' BX AX; auto; left; apply length_sym; auto). treat_equalities. assert (HProd2 : Prod O E E' T AXMBX CXMBX); [|split; auto]. { destruct (opp_exists O E E' HNC E) as [ME HME]; Col. assert (HColME : Col O E ME) by (unfold Opp, Sum, Ar2 in *; spliter; Col). apply prod_assoc1 with L3 IAB ME; auto; [|apply opp_prod; auto; apply diff_opp with BX CX; auto]. apply prod_assoc2 with L1 ME E; auto; apply opp_prod; auto. apply diff_opp with BX AX; auto. } destruct (opp_exists O E E' HNC E) as [ME HME]; Col. apply prod_assoc1 with IAB L3 XProd; auto; apply prod_comm; auto. apply prod_assoc1 with CYMBY L1 E; apply prod_comm; auto; try apply prod_1_l; Col; apply prod_assoc1 with AXMBX ME BYMCY; auto; [|apply prod_comm]; apply opp_prod; auto; [apply diff_opp with AX BX|apply diff_opp with CY BY]; auto. } { assert (L3 = CXMBX); treat_equalities. { apply opp_uniqueness with O E E' BXMCX; Col; apply opp_comm; auto. apply diff_opp with CX BX; auto. } assert (HLe6 : LtP O E E' BX CX). { assert (H : LeP O E E' BX CX). { apply compatibility_of_sum_with_order with O L3 BX; auto; try apply sum_O_B; Col; apply sum_comm; Col; apply diff_sum; auto. } elim H; clear H; intro H; auto; treat_equalities. exfalso; apply HDiff7; apply diff_uniqueness with O E E' BX BX; auto. apply diff_null; Col. } assert (HLe7 : LeP O E E' BX AX) by(apply bet_lt12_le13 with CX; auto). assert (L1 = AXMBX) by (apply l16_9_1 with O E E' AX BX; auto; left; auto). treat_equalities. split; auto. destruct (opp_exists O E E' HNC E) as [ME HME]; Col. destruct (opp_exists O E E' HNC XProd) as [MProd HMProd]; Col. apply prod_assoc1 with IAB L3 MProd; apply prod_comm; auto; [apply prod_assoc2 with BXMCX ME XProd; auto; apply opp_prod; auto; apply diff_opp with BX CX; auto|]. apply prod_assoc1 with CYMBY L1 E; apply prod_comm; auto; try apply prod_1_l; Col. apply prod_assoc2 with BYMCY ME XProd; auto; apply opp_prod; auto. apply diff_opp with BY CY; auto. } } } } } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths