proposition: Lemma BRabs_neg x: inc x BRm -> BRabs x = BRopp x.
proof: Proof. case (equal_or_not x \0r) => e1. by rewrite e1 BRopp_0 BRabs_0. by move => h; apply:BRabs_negs; apply /BRms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)