proposition: Lemma ghalfa_exists : forall A O B, ~ Bet A O B -> exists A' O' B', gHalfA A' O' B' A O B.
proof: Proof. intros A O B H. destruct (halfa_exists A O B H) as [P HP]. exists A, O, P. apply halfa__ghalfa, HP. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma