proposition: Lemma ghalfa_right_comm : forall A' O' B' A O B, gHalfA A' O' B' A O B -> gHalfA A' O' B' B O A.
proof: Proof. intros A' O' B' A O B [P [[HNBet [HP1 HP2]] HP3]]. exists P. split; [split; [|split]|]. Between. apply l11_24, HP1. CongA. apply conga_trans with A O P; assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.suma