proposition: Lemma Z2intK : cancel Z2int int2Z.
proof: Proof. case => [|p|p] //=. { have Pp := nat_of_pos_gt0 p. by rewrite /= -(prednK Pp) (prednK Pp) -binnat.to_natE Pos2Nat.id. } rewrite /int2Z. have Pp := nat_of_pos_gt0 p. rewrite -(prednK Pp) {Pp} /= -!binnat.to_natE. rewrite -[in RHS](Pos2Nat.id p). set n := Pos.to_nat p. by case: n. 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)