proposition: Lemma ghalfa_comm : forall A' O' B' A O B, gHalfA A' O' B' A O B -> gHalfA B' O' A' B O A.
proof: Proof. intros A' O' B' A O B H. apply ghalfa_left_comm, ghalfa_right_comm, H. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma