proposition: Theorem lucas_theorem (l m : list nat) : Forall (fun i => i < p) l -> Forall (fun i => i < p) m -> rem (binomial (base_p l) (base_p m)) p = rem (binomial_p l m) p.
proof: Proof. Proof using Hp. intros H; revert H m. induction 1 as [ | x l H1 H2 IH2 ]; induction 1 as [ | y m H3 H4 IH4 ]. + simpl; auto. + rewrite binomial_p_fix01; simpl base_p. rewrite <- rem_mult_rem, <- IH4, rem_mult_rem, (Nat.mul_comm p), Nat.add_comm, (Nat.mul_comm (binomial _ _)). apply lucas_lemma; auto; simpl; lia. + rewrite binomial_p_fix10; simpl base_p. rewrite <- rem_mult_rem, <- IH2, rem_mult_rem; auto. rewrite (Nat.mul_comm p), Nat.add_comm, (Nat.mul_comm (binomial _ _)). apply lucas_lemma; auto; simpl; lia. + rewrite binomial_p_fix11; simpl base_p. rewrite <- rem_mult_rem, <- IH2, rem_mult_rem; auto. rewrite !(Nat.mul_comm p), !(Nat.add_comm _ (_ * _)), (Nat.mul_comm (binomial _ _)). apply lucas_lemma; auto; simpl; lia. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)