proposition: Fact expoZ_power n x : expoZ n (Z.of_nat x) = Z.of_nat (power n x).
proof: Proof. symmetry; apply mscal_morph; auto. intros; apply Nat2Z.inj_mul. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)