proposition: Lemma ghalfa_chara : forall A' O' B' A O B, gHalfA A' O' B' A O B <-> (Acute A' O' B' /\ SumA A' O' B' A' O' B' A O B).
proof: Proof. intros A' O' B' A O B. split. intro HHalf; split; [eapply ghalfa__acute, HHalf|apply ghalfa__suma, HHalf]. intros [HAcute HSuma]. destruct (halfa_exists A O B) as [P HP]. apply (acute_suma__nbet A' O' B'); assumption. exists P; split; [assumption|]. apply sams2_suma2__conga with A O B; [SumA..| |]. eapply halfa__sams, HP. apply halfa__suma, HP. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma