proposition: Lemma BRdiff_div a b c: realp a -> realp b -> realp c -> c <> \0r -> a -r (b /r c) = (a *r c -r b) /r c.
proof: Proof. move => ar br cr cnz. by rewrite /BRdiff (BRopp_div_l br cr); apply: BRsum_div => //; apply:RSo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)