proposition: Lemma halfa_sym : forall A O B P, HalfA P A O B -> HalfA P B O A.
proof: Proof. unfold HalfA. intros. spliter. split; [|split]. intro; Between. apply l11_24; assumption. apply conga_sym; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma