proposition: Lemma ghalfa__out : forall A O B, gHalfA A O B A O B -> Out O A B.
proof: Proof. intros A O B HHalf. rewrite ghalfa_chara in HHalf; spliter. apply (sams_suma__out546 A O B); SumA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma