proposition: Lemma BRprod_mlt2r 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_Mltlt0. move => h; case: (rleT_el pb pa) => //. move /(BRprod_mle2r pb pa pc) => h2; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)