proposition: Lemma suma_assoc_1 : forall A B C D E F G H I K L M A' B' C' D' E' F', SAMS A B C D E F -> SAMS D E F G H I -> SumA A B C D E F A' B' C' -> SumA D E F G H I D' E' F' -> SumA A' B' C' G H I K L M -> SumA A B C D' E' F' K L M.
proof: Proof. intros A B C D E F G H I K L M A' B' C' D' E' F' HisiBE HisiEH HsBE HsEH HsB'H. assert(HA0 : exists A0, Midpoint B A A0) by apply symmetric_point_construction. destruct HA0 as [A0 []]. assert(HD0 : exists D0, Midpoint E D D0) by apply symmetric_point_construction. destruct HD0 as [D0 []]. assert_diffs. elim(col_dec A B C). { intro HColB. elim(bet_dec A B C). { intro HBBet. destruct HisiBE as [_ [[HEout | HBNBet] HJ]]; try solve [exfalso; Between]. apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto. apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto. apply (out213_suma__conga D E F); auto. } intro HBout. apply not_bet_out in HBout; auto. assert(Hexsuma : exists K0 L0 M0, SumA A B C D' E' F' K0 L0 M0) by (apply ex_suma; auto). destruct Hexsuma as [K0 [L0 [M0]]]. apply (conga3_suma__suma A B C D' E' F' K0 L0 M0); try (apply conga_refl); auto. apply (conga_trans _ _ _ D' E' F'). apply conga_sym; apply (out213_suma__conga A B C); auto. apply (suma2__conga D E F G H I); auto. apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto. apply conga_sym. apply (out213_suma__conga A B C); auto. } intro HNColB. assert(~ Col C B A0) by (intro; apply HNColB; apply (l6_16_1 _ A0); Col). elim(col_dec D E F). { intro HColE. elim(bet_dec D E F). { intro HEBet. destruct HisiEH as [_ [[HHout | HENBet] HJ]]; try solve [exfalso; Between]. apply (conga3_suma__suma A B C D E F A' B' C'); try (apply conga_refl); try (apply (out546_suma__conga _ _ _ G H I)); auto. } intro HEout. apply not_bet_out in HEout; auto. apply (conga3_suma__suma A' B' C' G H I K L M); try (apply conga_refl); auto. apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto. apply (out213_suma__conga D E F); auto. } intro HNColE. assert(~ Col F E D0) by (intro; apply HNColE; apply (l6_16_1 _ D0); Col). elim(col_dec G H I). { intro HColH. elim(bet_dec G H I). { intro HHBet. apply sams_sym in HisiEH. destruct HisiEH as [_ [[HEout | HHNBet] HJ]]; try solve [exfalso; Between]. exfalso. apply HNColE. apply col_permutation_4. apply out_col; auto. } intro HHout. apply not_bet_out in HHout; auto. apply (conga3_suma__suma A B C D E F A' B' C'); try (apply conga_refl); try (apply (out546_suma__conga _ _ _ G H I)); auto. } intro HNColH. assert(~ OS B C A A0). { apply l9_9. repeat split; Col. exists B. split; Col; Between. } assert(TS E F D D0) by (apply bet__ts; Col). elim(col_dec A' B' C'). { intro HColB'. elim(bet_dec A' B' C'). { intro HB'Bet. elim(col_dec D' E' F'). { intro HColE'. elim(bet_dec D' E' F'). { intro HE'Bet. apply suma_sym. apply (conga3_suma__suma A' B' C' G H I K L M); [CongA..| |CongA]. apply conga_sym. apply (conga_trans _ _ _ D0 E F). - apply (sams2_suma2__conga123 _ _ _ _ _ _ D E F A' B' C'); [SumA..|]. apply suma_sym. exists D0. repeat (split; CongA); Side; Cop. - apply (sams2_suma2__conga456 D E F _ _ _ _ _ _ D' E' F'); auto. SumA. exists D0. repeat (split; CongA); Side; Cop. } intro HE'out. apply not_bet_out in HE'out; auto. exfalso. apply HNColE. apply col_permutation_4. apply out_col. apply (out_lea__out _ _ _ D' E' F'); auto. apply (sams_suma__lea123789 _ _ _ G H I); auto. } intro HNColE'. assert(CongA D E F C B A0). { apply (sams2_suma2__conga456 A B C _ _ _ _ _ _ A' B' C'); auto. SumA. apply (conga3_suma__suma A B C C B A0 A B A0); [SumA|CongA..]. } assert(HJ : SAMS C B A0 G H I) by (apply (conga2_sams__sams D E F G H I); try (apply conga_refl); auto). destruct HJ as [_ [_ [J]]]. destruct HisiEH as [_ [_ [F1]]]. spliter. assert_diffs. assert(CongA C B J D' E' F'). { apply (conga_trans _ _ _ D E F1); auto. - apply (l11_22 _ _ _ A0 _ _ _ F); auto. split. left; split; apply cop_nos__ts; Cop; apply (ncol_conga_ncol G H I); CongA. split. CongA. apply (conga_trans _ _ _ G H I); CongA. - apply (suma2__conga D E F G H I); auto. exists F1. repeat (split; CongA). } apply (conga3_suma__suma A B C D' E' F' A B J); [|apply conga_refl; auto..|]. { exists J. assert (TS C B J A). { apply (l9_8_2 _ _ A0). apply l9_2, invert_two_sides, bet__ts; Col. apply cop_nts__os; Col. apply not_col_permutation_2. apply (ncol_conga_ncol D' E' F'); CongA. } repeat (split; CongA); Side; Cop. } apply (suma2__conga A' B' C' G H I); auto. apply (conga3_suma__suma A B A0 A0 B J A B J); [|CongA..]. exists J. repeat (split; CongA); Cop. apply col123__nos; Col. } intro HB'out. apply not_bet_out in HB'out; auto. exfalso. apply HNColB. apply col_permutation_4. apply out_col. apply (out_lea__out _ _ _ A' B' C'); auto. apply (sams_suma__lea123789 _ _ _ D E F); auto. } intro HNColB'. clear dependent A0. destruct HisiBE as [_ [_ [C1 HC1]]]. spliter. assert_diffs. assert(CongA A' B' C' A B C1). { apply (suma2__conga A B C D E F); auto. apply (conga3_suma__suma A B C C B C1 A B C1); CongA. exists C1. repeat (split; CongA). } assert(OS B C1 C A). { apply one_side_symmetry. apply os_ts1324__os. - apply invert_one_side. apply cop_nts__os; Col. apply not_col_permutation_2; apply (ncol_conga_ncol A' B' C'); auto. - apply cop_nos__ts; Col; Cop. apply (ncol_conga_ncol D E F); CongA. } elim(col_dec D' E' F'). { intro HColE'. elim(bet_dec D' E' F'). { intro HE'Bet. assert(HC0 : exists C0, Midpoint B C C0) by apply symmetric_point_construction. destruct HC0 as [C0 []]. assert_diffs. assert(TS B C1 C C0). { apply bet__ts; auto. apply not_col_permutation_1, (ncol_conga_ncol D E F); CongA. } apply (conga3_suma__suma A B C C B C0 A B C0); [|CongA..|]. exists C0; repeat (split; CongA); Cop; apply col124__nos; Col. apply (suma2__conga A' B' C' G H I); auto. apply (conga3_suma__suma A B C1 C1 B C0 A B C0); [|CongA| |CongA]. apply ts__suma, invert_two_sides, (l9_8_2 _ _ C); auto. apply (sams2_suma2__conga456 C B C1 _ _ _ _ _ _ C B C0). SumA. apply (conga2_sams__sams D E F G H I); CongA. SumA. apply (conga3_suma__suma D E F G H I D' E' F'); CongA. } intro HE'out. apply not_bet_out in HE'out; auto. exfalso. apply HNColE. apply col_permutation_4. apply out_col. apply (out_lea__out _ _ _ D' E' F'); auto. apply (sams_suma__lea123789 _ _ _ G H I); auto. } intro HNColE'. clear dependent D0. assert(HJ : SAMS C B C1 G H I) by (apply (conga2_sams__sams D E F G H I); CongA). destruct HJ as [_ [_ [J]]]. destruct HisiEH as [_ [_ [F1 HF1]]]. spliter. assert_diffs. assert(CongA C B J D' E' F'). { apply (conga_trans _ _ _ D E F1); auto. - apply (l11_22 _ _ _ C1 _ _ _ F); auto. split. left; split; apply cop_nos__ts; Cop; [apply (ncol_conga_ncol D E F)|apply (ncol_conga_ncol G H I)..]; CongA. split. CongA. apply (conga_trans _ _ _ G H I); CongA. - apply (suma2__conga D E F G H I); auto. exists F1. repeat (split; CongA). } assert (~ Col C B C1) by (apply (ncol_conga_ncol D E F); CongA). apply (conga3_suma__suma A B C C B J A B J); try (apply conga_refl); auto. - assert (TS B C J A). { apply (l9_8_2 _ _ C1). apply l9_2; apply cop_nos__ts; Col; Cop. apply invert_one_side. apply cop_nts__os; Col; Cop. apply not_col_permutation_2, (ncol_conga_ncol D' E' F'); CongA. } exists J. repeat (split; CongA); Side; Cop. - apply (suma2__conga A' B' C' G H I); auto. apply (conga3_suma__suma A B C1 C1 B J A B J); CongA. assert (TS B C1 A J). { apply (l9_8_2 _ _ C); auto. apply cop_nos__ts; Cop. apply (ncol_conga_ncol G H I); CongA. } exists J. repeat (split; CongA); Side; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles