proposition: Lemma rlt0xP x: \0r <r x <-> inc x BRps.
proof: Proof. split; first by move => [/rle0xP pa /nesym pb]; apply /BRps_iP. by move /BRps_iP => [/rle0xP h /nesym]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)