proposition: Lemma bet_out__bet : forall A B C P, Bet A P C -> Out P A B -> Bet B P C.
proof: Proof. intros A B C P HBet HOut. destruct (eq_dec_points C P). subst; Between. apply (l6_2 A); trivial; destruct HOut as [HPA [HPB]]; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le