proposition: Lemma halfa__nbet2 : forall A O B P, HalfA P A O B -> ~ Bet A O P /\ ~ Bet B O P.
proof: Proof. intros A O B P. split. apply (halfa__nbet A O B P); auto. apply halfa_sym in H. apply (halfa__nbet B O A P); auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma