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