proposition: Lemma BRsum_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. have {1} -> : a = (a *r c) /r c by rewrite BRprodC BRdiv_prod //. by rewrite - BRprodDl //; [ apply:RS_inv| apply:RSp]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)