proposition: Fact alpha_Z_S n : α (S n) = Z.of_nat (alpha_nat n).
proof: Proof. auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)