proposition: Lemma rgt0xP x: x <r \0r <-> inc x BRms.
proof: Proof. split; last by move => /setC_P [sa sb]; case: (rleT_el RS0 sa) => // /rle0xP. move => sa; move:(proj31_1 sa) => xr. apply/setC_P; split => //; move/rle0xP => h; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)