proposition: Fact binomial_Zp_zero :〚binomial n k〛= Zp.
proof: Proof. Proof using Hkn Hprime. generalize binomial_with_p'; intros G. apply f_equal with (f := nat2Zp Hp) in G. repeat rewrite nat2Zp_mult in G. rewrite nat2Zp_p in G. repeat rewrite Zp_mult_zero in G. apply Zp_invertible_eq_zero in G; auto. repeat (apply Zp_mult_invertible; auto). Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)