proposition: Lemma BR_i2P x: realp x <-> (inc x BRps \/ inc x BRm).
proof: Proof. split; last by case; [apply:BRps_sBR | apply:BRm_sBR ]. by case/BR_i1P => h; [ right; rewrite h; apply:RmS0 | left | right; apply: BRms_sBRm] => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)