proposition: Fact binomial_p_fix01 y m : binomial_p nil (y::m) = binomial 0 y * binomial_p nil m.
proof: Proof. auto. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)