proposition: Lemma BRprod_Mltlt0 a b c: inc c BRms -> a <r b -> (b *r c) <r (a *r c).
proof: Proof. move => cm; move: (BRopp_negative1 cm) => ocp ineq. move: (BRprod_Mltgt0 ocp (rlt_opp ineq)). move: ineq => [[ar br _] _]; move: (BRms_sBR cm) => cr. rewrite BRprod_opp_opp // BRprod_opp_opp //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)