proposition: Lemma ex_suma : forall A B C D E F, A<>B -> B<>C -> D<>E -> E<>F -> exists G H I, SumA A B C D E F G H I.
proof: Proof. intros A B C D E F HAB HBC HDE HEF. exists A. exists B. elim (col_dec A B C). { intro HColB. destruct (angle_construction_4 D E F C B A) as [J [HConga HCop]]; auto. assert_diffs. exists J. exists J. repeat (split; CongA); Cop. apply (col123__nos); Col. } intro HNColB. elim (col_dec D E F). { intro HColE. elim (bet_dec D E F). { intro HEBet. assert (HJ : exists J, Midpoint B C J) by (apply symmetric_point_construction). destruct HJ as [J HMid]. assert_diffs. destruct HMid as [HJBet HCong]. exists J, J. split. CongA. split. apply col124__nos; Col. split; CongA; Cop. } intro HENBet. assert (HEOut : Out E D F) by (apply l6_4_2; auto). exists C. exists C. split. apply l11_21_b; [apply out_trivial|]; auto. split. apply col124__nos; Col. split; CongA; Cop. } intro HNColE. assert (HJ : exists J, CongA D E F C B J /\ TS C B J A) by (apply ex_conga_ts; Col). destruct HJ as [J [HConga HTwo]]. assert_diffs. exists J, J. repeat (split; CongA); [Side|Cop]. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles