proposition: Lemma BRprod_Mpp b c: inc b BRp -> \1r <=r c -> b <=r (b *r c).
proof: Proof. move => pa pb. by rewrite BRprodC - {1} (BRprod_1l (BRp_sBR pa)); apply: BRprod_Mlege0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)