proposition: Lemma BRdiv_sumDl x y z: realp x -> realp y -> realp z -> (y +r z) /r x = (y /r x) +r (z /r x).
proof: Proof. move => xr yr zr;rewrite /BRdiv BRprodDl //; exact:RS_inv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)