proposition: Lemma BRmpS_div a b: inc a BRm -> inc b BRp -> inc (a /r b) BRm.
proof: Proof. move: RmS0 => izp ap bp. case: (equal_or_not a \0r) => az; first by rewrite az BRdiv_0x. case: (equal_or_not b \0r) => bz; first by rewrite bz BRdiv_x0. by apply/(BRms_sBRm); apply:RmpsS_div; [ apply/BRms_iP | apply/BRps_iP ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)