proposition: Lemma suma_suppa__bet : forall A B C D E F G H I, SuppA A B C 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 [_ [A' [HBet HCong]]] [A'' [HConga1 [HNOS [HCop HConga2]]]]. apply (bet_conga__bet A B A''); trivial. assert_diffs. apply between_symmetry, l6_2 with A'; Between. destruct (conga_cop__or_out_ts C B A' A'') as [|HTS]; auto. apply coplanar_perm_3, col_cop__cop with A; Col; Cop. apply conga_trans with D E F; CongA. exfalso. apply HNOS. exists A'; split; [|Side]. destruct HTS as [HNCol1 [HNCol2 _]]. repeat split. intro; apply HNCol1; ColR. Col. exists B; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles