proposition: Lemma suma_sym : forall A B C D E F G H I, SumA A B C D E F G H I -> SumA D E F A B C G H I.
proof: Proof. intros A B C D E F G H I Hsuma. destruct Hsuma as [J [HCongaBCJ [HNOne [HCongaABJ HCop]]]]. assert_diffs. elim (col_dec A B C). { intro HColB. elim (bet_dec A B C). { intro HBBet. assert (HK : exists K, Midpoint E F K) by (apply symmetric_point_construction). destruct HK as [K [HKBet HCong]]. assert_diffs. exists K. split; CongA. split. apply col124__nos; Col. split; Cop. apply (conga_trans D E K A B J); auto. apply conga_left_comm; apply (l11_13 F E D C B J); Between; CongA. } intro HBNBet. assert (HBOut : Out B A C) by (apply l6_4_2; auto). exists F. split. apply l11_21_b; Out. split. apply col124__nos; Col. split; Cop. apply (conga_trans D E F A B J); auto. apply conga_sym. apply (l11_10 C B J D E F); try (apply out_trivial); auto. } intro HNColB. elim (col_dec D E F). { intro HColE. assert (HK : exists K, CongA A B C F E K) by (apply angle_construction_3; auto). destruct HK as [K HConga]. assert_diffs. exists K. split; CongA. split. apply col123__nos; Col. split; Cop. apply (conga_trans D E K A B J); auto. elim (bet_dec D E F). { intro HEBet. apply conga_sym; apply conga_left_comm. apply (l11_13 C B A F); CongA; Between. apply (bet_conga__bet D E F); CongA. } intro HENBet. assert (HEOut : Out E D F) by (apply l6_4_2; auto). apply conga_sym. apply (l11_10 A B C F E K); try (apply out_trivial); auto. apply (l11_21_a D E F); CongA. } intro HNColE. assert (HK : exists K, CongA A B C F E K /\ TS F E K D) by (apply ex_conga_ts; Col). destruct HK as [K [HConga HTwo]]. exists K. split; CongA. split. apply l9_9; apply l9_2; apply invert_two_sides; auto. split; Cop. apply (conga_trans D E K A B J); auto. apply conga_sym; apply conga_right_comm. apply (l11_22a A B J C K E D F). split. apply cop_nos__ts; Col; Cop. intro; apply HNColE; apply (col_conga_col C B J D E F); Col. split. apply invert_two_sides; auto. split; CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles