proposition: Lemma bin_lucas m n k : (m < p ^ k -> n < p ^ k -> 'C(m, n) = \prod_(i < k) 'C(digitn p m i, digitn p n i) %[mod p])%N.
proof: Proof. move=> mLp nLp. have [nLm | mLn] := leqP n m; last first. suff [i Hi] : exists i : 'I_k, (digitn p m i < digitn p n i)%N. by rewrite (bigD1 i) //= !bin_small. apply/existsP; apply: contraTT mLn. rewrite negb_exists -leqNgt => /forallP dmLdn. rewrite (digitnE nLp) (digitnE mLp) leq_sum // => i _. by rewrite leq_mul2r leqNgt dmLdn orbT. have -> : ('C(m, n) %% p)%N = ((1 + 'X) ^+ m : {poly 'F_p})`_n. have nLm1 : (n < m.+1)%N by apply: leq_trans nLm. rewrite exprDn coef_sum. under eq_bigr do rewrite expr1n mul1r coefMn coefXn. rewrite (bigD1 (Ordinal nLm1)) //= eqxx mulr1n big1 => [|i /eqP/val_eqP/=]. by rewrite [X in (_ = _ %% X)%N]Fp_cast // addn0 val_Fp_nat // modn_mod. by rewrite eq_sym => /negPf->; rewrite mulr0n // mul0rn. rewrite {1}(digitnE mLp) expr_sum. under eq_bigr do rewrite mulnC exprM Fp_exprnDn // expr1n exprDn. have H i : \sum_(j < (digitn p m i).+1) 1 ^+ (digitn p m i - j) * 'X^(p ^ i) ^+ j *+ 'C(digitn p m i, j) = \sum_(j < p) 'X^(p ^ i) ^+ j *+ 'C(digitn p m i, j). under eq_bigr do rewrite expr1n mul1r. rewrite -!(big_mkord xpredT (fun j => 'X^(p ^ i) ^+ j *+ 'C(digitn p m i, j))). rewrite (big_cat_nat _ _ _ _ (ltn_pdigit m i (prime_gt0 Pp))) //=. rewrite [X in _ = _ + X]big_nat_cond [X in _ = _ + X]big1 ?addr0 // => j. by case/andP=> /andP[/bin_small->]; rewrite mulr0n. under eq_bigr do rewrite {}H. rewrite bigA_distr_bigA /= coef_sum. under eq_bigr do under eq_bigr do rewrite -exprM mulnC. under eq_bigr do rewrite prodrMn -expr_sum coefMn coefXn. pose f : {ffun 'I_k -> 'I_p} := [ffun i : 'I_k => Ordinal (ltn_pdigit n i (prime_gt0 Pp))]. rewrite (bigD1 f) //= [X in (_ %% X)%N]Fp_cast //= . rewrite [in X in ((_ + X) = _ %[mod _])%N]big1 ?addn0 => [| i iDf]. rewrite (_ : _ == _) ?mulr1n. under eq_bigr do rewrite ffunE /=. by rewrite val_Fp_nat // modn_mod. apply/eqP; rewrite {1}[n](digitnE nLp); apply: eq_bigr => /= i _. by rewrite ffunE. case: (n =P _) => nEs //; last by rewrite mul0rn. case/eqP: iDf; apply/ffunP => j; apply/val_eqP =>/=. by rewrite (digitn_uniq _ _ nEs) // ffunE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra)