proposition: Theorem lucas_lemma : rem (binomial n k) p = rem (binomial N K * binomial n0 k0) p.
proof: Proof. Proof using choice. destruct choice as [ (H1 & H2) | [ (H1 & H2) | (H1 & H2) ] ]; clear choice. 3: { rewrite binomial_gt with (1 := H2). f_equal. destruct H1 as [ H1 | H1 ]; rewrite binomial_gt with (1 := H1); ring. } + apply nat2Zp_inj with (Hp := Hp). rewrite nat2Zp_mult. apply binomial_Zp_prod; auto. + rewrite binomial_gt with (1 := H1). rewrite Nat.mul_0_r. apply nat2Zp_inj with (Hp := Hp). rewrite nat2Zp_zero. apply binomial_Zp_zero with (2 := G1) (3 := G3); auto. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)