proposition: Lemma nat_of_pos_Z_to_pos x : nat_of_pos x = `|Z2int (Z.pos x)|%N.
proof: Proof. by rewrite /absz /Z2int. 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)