proposition: Lemma BRdiff_diff_simp a b: realp a -> realp b -> a -r (a -r b) = b.
proof: Proof. by move => aq bq; rewrite (BRdiff_diff aq aq bq) (BRdiff_xx aq) BRsum_0l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)