proposition: Lemma suma2__conga : forall A B C D E F G H I G' H' I', SumA A B C D E F G H I -> SumA A B C D E F G' H' I' -> CongA G H I G' H' I'.
proof: Proof. intros A B C D E F G H I G' H' I' Hsuma Hsuma'. destruct Hsuma as [J [HJ1 [HJ2 [HJ3 HCop]]]]. destruct Hsuma' as [J' [HJ'1 [HJ'2 [HJ'3 HCop']]]]. assert_diffs. assert (HcongaC : CongA C B J C B J') by (apply (conga_trans C B J D E F); auto; apply conga_sym; auto). assert (HcongaA : CongA A B J A B J'). { elim (col_dec A B C). { intro HColB. elim (bet_dec A B C). { intro HBBet. apply (l11_13 C B J C B J'); Between. } intro HBNBet. assert (HBOut : Out B A C) by (apply l6_4_2; auto). apply (l11_10 C B J C B J'); try (apply out_trivial); auto. } intro HNColB. elim (col_dec D E F). { intro HColE. apply out2__conga; [apply out_trivial|]; auto. elim (bet_dec D E F). { intro HEBet. apply l6_3_2; repeat split; auto. exists C. split; auto; split; apply (bet_conga__bet D E F); CongA. } intro HENBet. assert (HEOut : Out E D F) by (apply l6_4_2; auto). apply l6_7 with C; apply (l11_21_a D E F); CongA. } intro HNColE. apply (l11_22a A B J C A B J' C); auto. repeat (split; try (apply cop_nos__ts); CongA); Cop; apply (ncol_conga_ncol D E F); CongA. } apply (conga_trans G H I A B J). CongA. apply (conga_trans A B J A B J'); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles