proposition: Lemma RpS_sum x y: inc x BRp -> inc y BRp -> inc (x +r y) BRp.
proof: Proof. move => /Zo_P [pa pb] /Zo_P[pc pd]; apply/Zo_P; split; first by apply: RSs. move => t /BR_sump [a /pb ax [b /pd bx ->]];apply:(QpS_sum ax bx). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)