proposition: Lemma BR_i0P x: realp x <-> (inc x BRms \/ inc x BRp).
proof: Proof. split; [move => ha | case; [apply:BRms_sBR | apply:BRp_sBR ]]. by case: (inc_or_not x BRp) => h; [ right | left;apply/setC_P]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)