proposition: Lemma BRprod_mle2r a b c: realp a -> realp b -> inc c BRms -> ((b *r c) <=r (a *r c) <-> a <=r b).
proof: Proof. move => pa pb pc; split; last by apply:BRprod_Mlele0; exact:(BRms_sBRm pc). move => h; case: (rleT_el pa pb) => // h1. move: (BRprod_Mltlt0 pc h1) => h2; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)