proposition: Lemma int2ZK : cancel int2Z Z2int.
proof: Proof. case => [n|n]; case: n => [|n] //=. case: n => [//|n]. { by rewrite -binnat.to_natE -Nat2Pos.inj_succ // Nat2Pos.id. } case: n => [//|n]. { by rewrite -binnat.to_natE -!Nat2Pos.inj_succ // 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)