proposition: Lemma BRsum_AC x y z: realp x -> realp y -> realp z -> (x +r y) +r z = (x +r z) +r y.
proof: Proof. move => xr yr zr. by rewrite - (BRsumA xr yr zr) - (BRsumA xr zr yr) (BRsumC y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)