proposition: Lemma ghalfa__suma : forall A' O' B' A O B, gHalfA A' O' B' A O B -> SumA A' O' B' A' O' B' A O B.
proof: Proof. intros A' O' B' A O B [P [HHalf HConga]]. assert (Hd := HHalf). apply halfa_distincts in HHalf. spliter. apply (conga3_suma__suma A O P A O P A O B); [|CongA..]. apply halfa__suma; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma