proposition: Lemma Z2int_abs x : Z2int (Z.abs x) = `|Z2int x|%nat.
proof: Proof. by case: x => // p /=; rewrite abszN. 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)