proposition: Lemma BRdiv_Mle1 a b c: realp a -> realp b -> inc c BRps -> ( a <=r b *r c <-> a /r c <=r b).
proof: Proof. move => ar br crp; move:(RpsS_inv crp) => ip. move/BRps_iP: (crp) => [/BRp_sBR cp cnz]. split => h. move: (BRprod_Mlege0 (BRps_sBRp ip) h). rewrite (BRprodC b) -! /(BRdiv _ _) BRdiv_prod //. move: (BRprod_Mlege0 (BRps_sBRp crp) h). rewrite BRprodC BRprod_div //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)