proposition: Lemma halfa__ghalfa : forall P A O B, HalfA P A O B -> gHalfA A O P A O B.
proof: Proof. intros P A O B HP. exists P. split; [assumption|]. apply halfa_distincts in HP. spliter. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma