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