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