proposition: Lemma rle0xP x: \0r <=r x <-> inc x BRp.
proof: Proof. split. rewrite BRzero_prop; move => [_ pa pb]; apply:Zo_i => //. apply: (sub_trans pb); apply: BQps_sBQp. move=> h; split; [apply:RS0 | exact:BRp_sBR | ]. rewrite BRzero_prop; exact:(BR_hi_Qps h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)