proposition: Lemma rge0xP x: x <=r \0r <-> inc x BRm.
proof: Proof. case: (equal_or_not x \0r) => xnz. rewrite xnz; split => _; [apply:RmS0 | apply: (rleR RS0)]. split => h; first by move /rgt0xP: (conj h xnz) => /BRms_sBRm. have /rgt0xP [//]: inc x BRms by apply/BRms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)