proposition: Lemma BRms_iP x: inc x BRms <-> inc x BRm /\ x <> \0r.
proof: Proof. split; first by move => h; split; [ by apply:BRms_sBRm | apply: BRms_nz]. move => [/setC_P [xr /BRps_iP h] x0]; apply /setC_P; split => // xp. by case: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)