proposition: Lemma BRdiv_Mltltge0 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: (drps) => [/BRp_sBR dr dnz]. move/ BRps_iP: (brps) => [/BRp_sBR br bnz]. have qr: realp (BRinv d) by apply:RS_inv. split; move => [sa sb];split. + by apply/(BRdiv_Mlelege0 ar brps cr drps). + dneg h; move: (f_equal (fun z => z /r d) h). rewrite BRprodC (BRdiv_prod dr ar dnz) => ->. by rewrite {2} /BRdiv - BRprodA // BRdiv_prod //; apply:RSp. + by apply/(BRdiv_Mlelege0 ar brps cr drps). + dneg h; move: (f_equal (fun z => z *r b) h). rewrite BRprodC BRprod_div // => ->. rewrite /BRdiv (BRprodC c)- (BRprodA qr cr br) (BRprodC (BRinv d)). by rewrite BRprodC (BRprodC b); apply: BRprod_div => //; apply:RSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)