proposition: Lemma BRdiv_div_simp a b c: realp a -> realp b -> realp c -> b <> \0r -> (a /r b) /r (c /r b) = a /r c.
proof: Proof. move => ar br cr bnz. move: (RS_inv br) (RS_inv cr) => bir cir. rewrite /BRdiv (BRinv_div cr br) (BRprodC a). rewrite (BRprod_ACA bir ar br cir) (BRprodC _ b) BRprod_inv1 //. by rewrite BRprod_1l //; apply:RSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)