proposition: Lemma Z2int_Z_of_nat n : Z2int (Z.of_nat n) = n.
proof: Proof. by case: n => //= n; rewrite Pos.of_nat_succ -binnat.to_natE Nat2Pos.id. 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)