fact: Definition alpha_Z n := match n with | 0%nat => -1 | S n => Z.of_nat (alpha_nat n) end.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)