proposition: Lemma BQabs_neg x: inc x BQm -> BQabs x = BQopp x.
proof: Proof. case (equal_or_not x \0q) => e1. by rewrite e1 BQopp_0 BQabs_0. by move => h; apply:BQabs_negs; apply /BQms_iP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)