proposition: Lemma sams_lea456_suma2__lea : forall A B C D E F G H I D' E' F' G' H' I', LeA D E F D' E' F' -> SAMS A B C D' E' F' -> SumA A B C D E F G H I -> SumA A B C D' E' F' G' H' I' -> LeA G H I G' H' I'.
proof: Proof. intros A B C D E F G H I D' E' F' G' H' I' Hlea Hisi' Hsuma Hsuma'. assert_diffs. elim(out_dec E' D' F'). { intro HE'out. apply conga__lea. apply (conga_trans _ _ _ A B C). apply conga_sym; apply (out546_suma__conga _ _ _ D E F); auto; apply (out_lea__out _ _ _ D' E' F'); auto. apply (out546_suma__conga _ _ _ D' E' F'); auto. } intro HE'Nout. elim(col_dec A B C). { intro HColB. destruct Hisi' as [_ [[HE'out|HBNBet]_]]. exfalso; auto. apply not_bet_out in HColB; auto. apply (l11_30 D E F D' E' F'); auto; apply (out213_suma__conga A B C); auto. } intro HNColB. elim(col_dec D' E' F'). { intro HColE'. apply sams_sym in Hisi'. destruct Hisi' as [_ [[HBout|HE'NBet]_]]; exfalso. apply HNColB; Col. apply not_bet_out in HColE'; auto. } intro HNColE'. clear HE'Nout. elim(col_dec D E F). { intro HColE. assert(~ Bet D E F) by (intro; apply HNColE'; apply bet_col; apply (bet_lea__bet D E F); auto). apply (l11_30 A B C G' H' I'); try (apply conga_refl); auto. apply (sams_suma__lea123789 _ _ _ D' E' F'); auto. apply (out546_suma__conga _ _ _ D E F); auto. apply not_bet_out; auto. } intro HNColE. elim(col_dec G' H' I'). { intro HColH'. elim(bet_dec G' H' I'). apply l11_31_2; auto. intro HH'out. apply not_bet_out in HH'out; auto. exfalso. apply HNColB. apply col_permutation_4. apply out_col. apply (out_lea__out _ _ _ G' H' I'); auto. apply (sams_suma__lea123789 _ _ _ D' E' F'); auto. } intro HNColH'. destruct Hisi' as [_[_[F'1]]]. spliter. apply(l11_30 _ _ _ _ _ _ D E F C B F'1) in Hlea; CongA. destruct Hlea as [F1]. spliter. assert_diffs. assert(CongA A B F'1 G' H' I'). apply (suma2__conga A B C D' E' F'); auto; exists F'1; repeat (split; CongA). assert(~ Col A B F'1) by (apply (ncol_conga_ncol G' H' I'); CongA). assert(~ Col C B F'1) by (apply (ncol_conga_ncol D' E' F'); CongA). apply (l11_30 A B F1 A B F'1); auto. - exists F1. split; CongA. apply l11_24. apply (in_angle_trans _ _ _ C). apply l11_24; auto. assert(Hts : TS B C A F'1) by (apply cop_nos__ts; Col; Cop). destruct Hts as [_ [_ [X]]]. spliter. repeat split; auto. exists X. split; Between. right. apply (col_one_side_out _ A); Col. apply invert_one_side. apply (one_side_transitivity _ _ _ F'1); auto. apply out_one_side; Col; apply bet_out; auto; intro; subst A; Col. apply one_side_symmetry; apply cop_nts__os; Col. - apply (suma2__conga A B C D E F); auto. assert (TS B C F1 A). { apply (l9_8_2 _ _ F'1). apply l9_2; apply cop_nos__ts; Col; Cop. apply invert_one_side; apply one_side_symmetry. apply in_angle_one_side; Col. apply not_col_permutation_4; apply (ncol_conga_ncol D E F); auto. } exists F1. repeat (split; CongA); Side; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles