proposition: Fact binomial_with_p : fact K * fact (N-(K+1)) * φ K k0 * Ψ K * φ (N-(K+1)) (p-(k0-n0)) * Ψ (N-(K+1)) * binomial n k = p * fact N * φ N n0 * Ψ N.
proof: Proof. Proof using Hkn. apply expo_p_cancel with (N-1). repeat rewrite Nat.mul_assoc. rewrite (Nat.mul_comm (expo _ _) p). rewrite <- mscal_S. rewrite H4, <- mprod_factorial_euclid, <- Hn. rewrite binomial_thm with (1 := Hkn). rewrite Hnk. rewrite Hk at 3. do 2 rewrite mprod_factorial_euclid. rewrite H5 at 1. rewrite power_plus. ring. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)