proposition: Lemma BRprod_Mgt0le a b c: realp a -> realp b -> inc c BRps -> ((c *r a) <=r (c *r b) <-> a <=r b).
proof: Proof. by move => pa pb pc; rewrite (BRprodC c) (BRprodC c); apply: BRprod_ple2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)