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