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