proposition: Lemma per2_suma__bet : forall A B C D E F G H I, Per A B C -> Per D E F -> SumA A B C D E F G H I -> Bet G H I.
proof: Proof. intros A B C D E F G H I HB HE HSuma. destruct HSuma as [A1 [HConga1 [HNos [HCop HConga2]]]]. assert_diffs. assert(Per A1 B C) by (apply (l11_17 D E F); CongA). apply (bet_conga__bet A B A1); auto. apply (col_two_sides_bet _ C). apply col_permutation_2; apply cop_per2__col with C; Cop. apply cop_nos__ts; Cop; apply per_not_col; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles