proposition: Lemma RmuS_div a b: inc a BRm -> inc b BRm -> inc (a /r b) BRp.
proof: Proof. move: RpS0 => 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/(BRps_sBRp); apply:RmsuS_div; apply/BRms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)