proposition: Lemma Z2int_div x y : Z.le 0 x -> Z.le 0 y -> Z2int (Z.div x y) = (Z2int x %/ Z2int y)%Z.
proof: Proof. case: x => [|x|//] _; [by rewrite intdiv.div0z|]. case: y => [|y|//] _; [by rewrite intdiv.divz0|]. rewrite -!positive_nat_Z -Nat2Z.inj_div; last first. rewrite !positive_nat_Z /= /divz gtr0_sgz ?mul1r; last first. { exact: nat_of_pos_gt0. } rewrite divE !binnat.to_natE absz_nat /Z2int. move: (Zle_0_nat (nat_of_pos x %/ nat_of_pos y)). rewrite -[X in _ = Posz X]Nat2Z.id. by case: Z.of_nat => //= p _; rewrite binnat.to_natE. 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)