proposition: Lemma RpmS_prod x y: inc x BRp -> inc y BRm -> inc (x *r y) BRm.
proof: Proof. move => sa sb. case: (equal_or_not x \0r) => h1; first by rewrite h1 BRprod_0l; apply: RmS0. case: (equal_or_not y \0r) => h2; first by rewrite h2 BRprod_0r; apply: RmS0. have xp: inc x BRps by apply/BRps_iP. have yp: inc y BRms by apply/BRms_iP. exact:(BRms_sBRm (RpmsS_prod xp yp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)