proposition: Lemma BRdiv_Mlelege0 a b c d: realp a -> inc b BRps -> realp c -> inc d BRps -> ( a /r b <=r c /r d <-> a *r d <=r b *r c).
proof: Proof. move => ar brps cr drps. move/ BRps_iP: (brps) => [/BRp_sBR br bnz]. move/ BRps_iP: (drps) => [/BRp_sBR dr dnz]. have idr:=RS_inv dr. have pb:=RSp cr br. have pa:=RSp pb idr. move:(BRprod_Mgt0le (RS_div ar br) (RS_div cr dr) brps). rewrite (BRprod_div br ar bnz) (BRprodA br cr idr) (BRprodC b). move:(BRprod_ple2r ar pa drps). rewrite -/(_ /r d) (BRprodC ((c *r b) /r d)) (BRprod_div dr pb dnz). move => sa sb; exact:(iff_sym(iff_trans sa sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)