proposition: Lemma Z2int_mul x y : Z2int (x * y) = (Z2int x * Z2int y)%R.
proof: Proof. case y=>/=. { by rewrite GRing.mulr0 Z.mul_0_r. } { by move=> p; rewrite Z2int_mul_nat_of_pos. } move=> p. by rewrite GRing.mulrN Z2int_mul_nat_of_pos -Z2int_opp Zopp_mult_distr_r. 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)