proposition: Fact binomial_Zp_prod :〚binomial n k〛=〚binomial N K〛⊗〚binomial n0 k0〛.
proof: Proof. Proof using Hkn Hn0 Hprime. generalize binomial_wo_p; intros G. apply f_equal with (f := nat2Zp Hp) in G. repeat rewrite nat2Zp_mult in G. repeat rewrite Psi_Zp_eq in G. repeat rewrite phi_Zp_eq in G. rewrite binomial_thm with (1 := H2) in G. repeat rewrite nat2Zp_mult in G. rewrite (Zp_mul_comm _ _〚 fact k0 〛) in G. repeat rewrite Zp_mul_assoc in G. rewrite (Zp_mul_comm _ _〚 fact k0 〛) in G. repeat rewrite <- Zp_mul_assoc in G. apply Zp_invertible_cancel_l in G. 2: apply Zp_invertible_factorial; auto; lia. repeat rewrite Zp_mul_assoc in G. do 2 rewrite (Zp_mul_comm _ _〚 fact _ 〛) in G. repeat rewrite <- Zp_mul_assoc in G. apply Zp_invertible_cancel_l in G. 2: apply Zp_invertible_factorial; auto; lia. repeat rewrite Zp_mul_assoc in G. rewrite <- mscal_plus in G; auto. replace (K+(N-K)) with N in G by lia. rewrite (Zp_mul_comm _ _ (expoZp _ _)) in G. apply Zp_invertible_cancel_l in G; trivial. apply Zp_expo_invertible, Zp_invertible_factorial; auto; lia. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)