proposition: Lemma out_dec : forall P A B, Out P A B \/ ~ Out P A B.
proof: Proof. intros. unfold Out. elim (bet_dec P A B);intro; elim (bet_dec P B A);intro; elim (eq_dec_points A P);intro; elim (eq_dec_points B P);intro; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le