proposition: Lemma Z2int_mul_nat_of_pos (x : BinNums.Z) (y : positive) : (Z2int x * nat_of_pos y)%R = Z2int (Z.mul x (BinNums.Zpos y)).
proof: Proof. rewrite /Z2int; case Ex: x. { by rewrite mul0r Z.mul_0_l. } { by rewrite /= -!binnat.to_natE Pos2Nat.inj_mul. } by rewrite /= mulNr -!binnat.to_natE Pos2Nat.inj_mul. 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)