proposition: Fact binomial_with_p' : φ K k0 * Ψ K * φ (N-(K+1)) (p-(k0-n0)) * Ψ (N-(K+1)) * binomial n k = p * binomial N K * (N-K) * φ N n0 * Ψ N.
proof: Proof. Proof using Hkn. apply (factorial_cancel (N-(K+1))); repeat rewrite Nat.mul_assoc. apply (factorial_cancel K); repeat rewrite Nat.mul_assoc. rewrite binomial_with_p. rewrite binomial_thm with (n := N) (p := K). 2: { apply Nat.lt_le_incl; auto. } rewrite HNK at 1. rewrite fact_S. rewrite <- HNK. ring. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)