proposition: Lemma sams2_suma2__conga456 : forall A B C D E F D' E' F' G H I, SAMS A B C 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 -> CongA D E F D' E' F'.
proof: Proof. intros A B C D E F D' E' F' G H I Hisi Hisi' Hsuma Hsuma'. assert_diffs. elim(col_dec A B C). { intro HColB. elim(bet_dec A B C). { intro HBBet. destruct Hisi as [_ [[HEout|]_]]; try solve [exfalso; Between]. destruct Hisi' as [_ [[HE'out|]_]]; try solve [exfalso; Between]. apply l11_21_b; auto. } intro HBout. apply not_bet_out in HBout; auto. apply (conga_trans _ _ _ G H I). - apply (out213_suma__conga A B C); auto. - apply conga_sym. apply (out213_suma__conga A B C); auto. } intro HNColB. destruct Hisi as [_[_[J [HJ1 [HJ2 [HJ3 HJ4]]]]]]. destruct Hisi' as [_[_[J' [HJ'1 [HJ'2 [HJ'3 HJ'4]]]]]]. assert_diffs. apply (conga_trans _ _ _ C B J); try solve [apply conga_sym; auto]. apply (conga_trans _ _ _ C B J'); auto. assert(CongA A B J A B J'). { apply (conga_trans _ _ _ G H I). apply (suma2__conga A B C D E F); auto; exists J; repeat (split; CongA). apply (suma2__conga A B C D' E' F'); auto; exists J'; repeat (split; CongA). } assert(HJJ' : Out B J J' \/ TS A B J J'). apply conga_cop__or_out_ts; auto; apply coplanar_trans_1 with C; Cop; Col. destruct HJJ' as [Hout|Hts]. - apply out2__conga; Out. - exfalso. apply HJ'3. apply (l9_8_2 _ _ J); auto. apply one_side_symmetry. apply cop_nts__os; Col. apply two_sides_not_col in Hts; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles