proposition: Lemma BRprod_Mlege0 a b c: inc c BRp -> a <=r b -> (a *r c) <=r (b *r c).
proof: Proof. move => cp ab; move: (ab) => [ar br _]; move: (BRp_sBR cp) => cr. move /(rle_diffP ar br): ab => p1. apply/ (rle_diffP (RSp ar cr) (RSp br cr)). by rewrite - BRprodBl //;apply:RpS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)