proposition: Lemma ghalfa__acute : forall A' O' B' A O B, gHalfA A' O' B' A O B -> Acute A' O' B'.
proof: Proof. intros A' O' B' A O B [P [HHalf HConga]]. apply (acute_conga__acute A O P); CongA. apply halfa__acute with B, HHalf. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma