proposition: Lemma Zabs_natE n : Z.abs_nat n = `|Z2int n|%N.
proof: Proof. case: n => //= p; first by rewrite binnat.to_natE. by rewrite abszN absz_nat binnat.to_natE. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)