proposition: Lemma col_trisuma__bet : forall A B C P Q R, Col A B C -> TriSumA A B C P Q R -> Bet P Q R.
proof: Proof. intros A B C P Q R HCol HTri. destruct HTri as [D [E [F []]]]. assert_diffs. destruct HCol as [|[|]]. - apply (bet_conga__bet A B C); auto. apply (conga_trans _ _ _ D E F). apply (out546_suma__conga _ _ _ B C A); try (apply bet_out); Between. apply (out546_suma__conga _ _ _ C A B); try (apply l6_6; apply bet_out); auto. - apply (bet_conga__bet B C A); auto. apply (conga_trans _ _ _ D E F). apply (out213_suma__conga A B C); try (apply l6_6; apply bet_out); auto. apply (out546_suma__conga _ _ _ C A B); try (apply bet_out); Between. - apply (bet_conga__bet C A B); auto. apply (out213_suma__conga D E F); auto. apply (l11_21_a B C A); try (apply l6_6; apply bet_out); auto. apply (out213_suma__conga A B C); try (apply bet_out); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles