proposition: Lemma Z2int_inj x y : Z2int x = Z2int y -> x = y.
proof: Proof. rewrite /Z2int. case x, y=>//. { move=>[] H. by rewrite -[Z0]/(Z.of_nat 0%N) H -binnat.to_natE positive_nat_Z. } { rewrite -binnat.to_natE /GRing.opp /= /intZmod.oppz /=. case E: (Pos.to_nat _)=>//=. by move: (binnat.to_nat_gt0 p); rewrite -E ltnn. } { rewrite -binnat.to_natE; case E: (Pos.to_nat _)=>//=. by move: (binnat.to_nat_gt0 p); rewrite -E ltnn. } { by move=>[] /nat_of_pos_inj ->. } { rewrite -!binnat.to_natE /GRing.opp /= /intZmod.oppz /=. case (Pos.to_nat p0)=>//=. by move=>[] H; move: (binnat.to_nat_gt0 p); rewrite H ltnn. } { rewrite -binnat.to_natE /GRing.opp /= /intZmod.oppz /=. case E: (Pos.to_nat _)=>//=. by move: (binnat.to_nat_gt0 p); rewrite -E ltnn. } { rewrite -!binnat.to_natE /GRing.opp /= /intZmod.oppz /=. case E: (Pos.to_nat p)=>//=. by move: (binnat.to_nat_gt0 p); rewrite -E ltnn. } rewrite -!binnat.to_natE /GRing.opp /= /intZmod.oppz /=. case E: (Pos.to_nat p)=>//=. { by move: (binnat.to_nat_gt0 p); rewrite -E ltnn. } case E': (Pos.to_nat p0)=>//= [] [] H. by move: E'; rewrite -H -E=>/Pos2Nat.inj ->. 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)