proposition: Lemma BR_i1P x: realp x <-> [\/ x = \0r, inc x BRps | inc x BRms].
proof: Proof. split. move => h; case: (equal_or_not x \0r) => xz; first by constructor 1. case: (inc_or_not x BRp) => xp; first by constructor 2; apply/setC1_P. by constructor 3; apply /setC_P. case;[ move ->; apply:RS0 | apply:BRps_sBR | apply:BRms_sBR ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)