proposition: Lemma RmsS_sum_r x y: inc x BRm -> inc y BRms -> inc (x +r y) BRms.
proof: Proof. move => pa pb. case: (equal_or_not x \0r) => h; first by rewrite h (BRsum_0l (BRms_sBR pb)). by apply:RmsS_sum_rl => //; apply/BRms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)