proposition: Lemma BRsumA x y z: realp x -> realp y -> realp z -> x +r (y +r z) = (x +r y) +r z.
proof: Proof. move => /BRi_sQ xr /BRi_sQ yr /BRi_sQ zr. set_extens t. move/BR_sump => [a ax [b /BR_sump [c cy [d dz -> ->]]]]. rewrite (BQsumA (xr _ ax) (yr _ cy) (zr _ dz)). apply/BR_sump; exists (a +q c); first by apply/BR_sump; ex_tac; ex_tac. ex_tac. move/BR_sump => [u /BR_sump [a ax [b iby ->]] [c cz ->]]. rewrite - (BQsumA (xr _ ax) (yr _ iby) (zr _ cz)). apply/BR_sump; ex_tac;exists (b +q c) => //;apply/BR_sump; ex_tac; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)