proposition: Lemma sams_assoc_1 : forall A B C D E F G H I 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' -> SAMS A' B' C' G H I -> SAMS A B C D' E' F'.
proof: Proof. intros A B C D E F G H I A' B' C' D' E' F' Hsams1 Hsams2 Hs1 Hs2 Hsams1'. assert_diffs. elim(col_dec A B C). { intro HColB. destruct Hsams1 as [_ [[HEout|HBout]_]]. - apply (conga2_sams__sams A' B' C' G H I); auto. apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto. apply (out213_suma__conga D E F); auto. - apply not_bet_out in HBout; auto. apply sams_sym. repeat split; auto. exists F'. split. apply l11_21_b; try (apply out_trivial); auto. split. apply col124__nos; Col. split; Cop. apply not_two_sides_id. } intro HNColB. elim(col_dec D E F). { intro HColE. destruct Hsams2 as [_ [[HHout|HEout]_]]. - apply (conga2_sams__sams A B C D E F); try (apply conga_refl); auto. apply (out546_suma__conga _ _ _ G H I); auto. - apply not_bet_out in HEout; auto. apply (conga2_sams__sams A' B' C' G H I); auto. apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto. apply (out213_suma__conga D E F); auto. } intro HNColE. elim(col_dec G H I). { intro HColH. apply sams_sym in Hsams2. destruct Hsams2 as [_ [[|HHout] _]]. exfalso; apply HNColE; Col. apply not_bet_out in HHout; auto. apply (conga2_sams__sams A B C D E F); try (apply conga_refl); auto. apply (out546_suma__conga _ _ _ G H I); auto. } intro HNColH. split; auto. split. right; intro; apply HNColB; Col. assert(~ Col A' B' C'). { intro. exfalso. destruct Hsams1' as [_ [[|HB'out] _]]. apply HNColH; Col. apply not_bet_out in HB'out; auto. 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. } assert(HC1 : exists C1, CongA C B C1 D E F /\ ~ OS B C A C1 /\ ~ TS A B C C1 /\ Coplanar A B C C1). destruct Hsams1 as [_ []]; auto. destruct HC1 as [C1]. spliter. assert_diffs. assert(CongA A B C1 A' B' C'). apply (suma2__conga A B C D E F); auto; exists C1; repeat (split; CongA). assert(HJ : exists J, CongA C1 B J G H I /\ ~ OS B C1 C J /\ ~ TS C B C1 J /\ Coplanar C B C1 J). { apply (conga2_sams__sams _ _ _ _ _ _ C B C1 G H I) in Hsams2; CongA. destruct Hsams2 as [_ [_ HJ]]; auto. } destruct HJ as [J [HJ1 [HJ2 [HJ3 HJ4]]]]. spliter. apply (conga2_sams__sams _ _ _ _ _ _ A B C1 C1 B J) in Hsams1'; CongA. destruct Hsams1' as [_ [_ [J']]]. spliter. assert_diffs. assert (~ Col A B C1) by (apply (ncol_conga_ncol A' B' C'); CongA). assert (~ Col C B C1) by (apply (ncol_conga_ncol D E F); CongA). assert (Coplanar C1 B A J) by (apply coplanar_trans_1 with C; Cop; Col). assert (HUn : Out B J' J \/ TS C1 B J' J). apply conga_cop__or_out_ts; auto. apply coplanar_trans_1 with A; Cop; Col. destruct HUn as [HJJ'|Hts]. { exists J. split; [|repeat split]. - apply (suma2__conga D E F G H I); auto. apply (conga3_suma__suma C B C1 C1 B J C B J); try (apply conga_refl); auto. exists J. repeat (split; CongA). - elim(col_dec C B J). intro; apply col124__nos; Col. intro. apply l9_9. apply l9_2. apply (l9_8_2 _ _ C1). apply l9_2; apply cop_nos__ts; Col; Cop. apply invert_one_side. apply cop_nts__os; Col; Cop. - elim(col_dec A B J). intro; intro Hts; destruct Hts; spliter; Col. intro. apply l9_9_bis. apply (one_side_transitivity _ _ _ C1). apply cop_nts__os; Col. apply (one_side_transitivity _ _ _ J'); [|apply invert_one_side; apply out_one_side; Col]. apply cop_nts__os; Col. apply not_col_permutation_2; apply (ncol_conga_ncol A B J); auto. apply out2__conga; [apply out_trivial|]; auto. - apply coplanar_trans_1 with C1; Cop; Col. } exfalso. apply l9_2 in Hts. apply invert_two_sides in Hts. apply HJ2. exists J'. split; auto. apply (l9_8_2 _ _ A). - apply cop_nos__ts; Cop. apply (ncol_conga_ncol G H I); auto. apply (conga_trans _ _ _ C1 B J); CongA. - apply os_ts1324__os. apply invert_one_side; apply cop_nts__os; Col. apply cop_nos__ts; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles