proposition: Lemma sams_suma__lea123789 : forall A B C D E F G H I, SumA A B C D E F G H I -> SAMS A B C D E F -> LeA A B C G H I.
proof: Proof. intros A B C D E F G H I Hsuma Hisi. assert_diffs. spliter. elim(col_dec A B C). { intro HColB. elim(bet_dec A B C). { intro HBBet. destruct Hisi as [_[[HEout|]]]; try solve[exfalso; auto]. apply conga__lea. apply (out546_suma__conga _ _ _ D E F); auto. } intro HBout. apply l11_31_1; auto. apply not_bet_out; auto. } intro HNColB. elim(col_dec D E F). { intro HColE. elim(bet_dec D E F). { intro HEBet. apply sams_sym in Hisi. destruct Hisi as [_[[HBout|]]]; try solve[exfalso; auto]. apply l11_31_1; auto. } intro HEout. apply conga__lea. 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 HHout. apply not_bet_out in HHout; auto. exfalso. destruct Hisi as [_ [HUn _]]. destruct HUn as [HEout | HBNBet]. apply HNColE; apply col_permutation_4; apply out_col; auto. destruct Hsuma as [J [HJ1 [HJ2 [HJ3 HJ4]]]]. apply HJ2. apply conga_sym in HJ4. apply l11_21_a in HJ4; auto. apply (l9_19 _ _ _ _ B); try split; Col. } intro HNColH. destruct Hisi as [_ [_ [J [HJ1 [HJ2 [HJ3 HJ4]]]]]]. assert_diffs. assert(HNColJ : ~ Col J B C). { intro HColJ. apply HNColE. apply (col_conga_col J B C); CongA. } assert(HCongaJ : CongA A B J G H I). { apply (suma2__conga A B C D E F); auto. exists J. repeat (split; CongA). } assert(HNColJ2 : ~ Col J B A). { intro HColJ. apply HNColH. apply (col_conga_col A B J); Col. } apply (l11_30 A B C A B J); CongA. exists C. split; CongA. apply cop_nos__ts in HJ2; Cop. destruct HJ2 as [a [b [X [HColX HXBet]]]]. repeat split; auto. exists X. split; auto. right. assert(HNColX : ~Col X A B). { intro. apply HNColJ2. apply col_permutation_1; apply (col_transitivity_1 A X); Col. intro; subst X; Col. } assert_diffs. apply (col_one_side_out _ A); Col. apply invert_one_side. apply (one_side_transitivity _ _ _ J). - apply out_one_side. left; Col. apply bet_out; auto. - apply one_side_symmetry. apply cop_nts__os; Col; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles