proposition: Lemma BRabs_diff a b: realp a -> realp b -> BRabs (a -r b) = BRabs (b -r a).
proof: Proof. by move => ar br; rewrite - (BRoppB br ar) (BRabs_opp (RS_diff br ar)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)