proposition: Lemma halfa__nbet : forall A O B P, HalfA P A O B -> ~ Bet A O P.
proof: Proof. unfold HalfA. intros A O B P H. spliter. intro HBet. apply (not_bet_and_out A O P). split. assumption. apply in_angle_out with B; trivial. assert_diffs. apply l6_2 with P; auto. apply (bet_conga__bet A O P); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma