proposition: Lemma halfa_exists : forall A O B, ~ Bet A O B -> exists P, HalfA P A O B.
proof: Proof. intros A O B HNBet. assert_diffs. destruct (angle_bisector A O B) as [P [HIn HConga]]; auto. apply conga_comm in HConga. exists P; repeat (split; trivial). Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma