proposition: Lemma BRprod_Mlele0 a b c: inc c BRm -> a <=r b -> (b *r c) <=r (a *r c).
proof: Proof. move => cm; move: (BRopp_negative2 cm) => ocp ineq. move: (BRprod_Mlege0 ocp (rle_opp ineq)). move: ineq => [ar br _]; move: (BRm_sBR cm) => cr. rewrite BRprod_opp_opp // BRprod_opp_opp //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)