(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

(** ** Luca's theorem *)

Require Import Arith Nat Omega Lia List.
Require Import utils_tac gcd prime binomial sums Zp rel_iter.

Set Implicit Arguments.

Local Notation power := (mscal mult 1).
Local Notation expo := (mscal mult 1).

Section fact.

  Let factorial_cancel n a b : fact n * a = fact n * b -> a = b.
  Proof.
(* Goal: forall _ : @eq nat (mul (@mscal nat mul (S O) n p) a) (mul (@mscal nat mul (S O) n p) b), @eq nat a b *)
    apply Nat.mul_cancel_l.
(* Goal: not (@eq nat (fact n) O) *)
    generalize (fact_gt_0 n); intro; lia.
  Qed.
  
  Notation Π := (msum mult 1).

  Notation mprod_an := (fun a n => Π n (fun i => i+a)).

  Fact mprod_factorial n : fact n = mprod_an 1 n.
  Proof.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i0 : nat => add i0 (add (mul i p) (S O))))) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i : nat => add i (S O)))) *)
    induction n as [ | n IHn ].
    + rewrite msum_0; auto.
    + rewrite msum_plus1; auto.
(* Goal: @eq nat (fact (S n)) (mul (@msum nat mul (S O) n (fun i : nat => add i (S O))) (add n (S O))) *)
      rewrite mult_comm, <- IHn, fact_S.
(* Goal: @eq nat (rem (Nat.add (S O) n) p) (rem (add n (S O)) p) *)
      f_equal; lia.
  Qed.

  Variable (p : nat) (Hp : p <> 0).

  Notation "〚 x 〛" := (nat2Zp Hp x).

  Let expo_p_cancel n a b : expo n p * a = expo n p * b -> a = b.
  Proof.
(* Goal: forall _ : @eq nat (mul (@mscal nat mul (S O) n p) a) (mul (@mscal nat mul (S O) n p) b), @eq nat a b *)
    apply Nat.mul_cancel_l.
(* Goal: not (@eq nat (@mscal nat mul (S O) n p) O) *)
    generalize (power_ge_1 n Hp); intros; lia.
  Qed.

  Fact mprod_factorial_Zp i n :〚mprod_an (i*p+1) n〛=〚fact n〛.
  Proof.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp ((fun a n : nat => @msum nat mul (S O) n (fun i : nat => add i a)) (add (mul i p) (S O)) n)) (@nat2Zp p Hp (fact n)) *)
    rewrite mprod_factorial.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i0 : nat => add i0 (add (mul i p) (S O))))) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i : nat => add i (S O)))) *)
    induction n as [ | n IHn ].
    + do 2 rewrite msum_0; auto.
    + do 2 (rewrite msum_plus1; auto).
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (mul (@msum nat mul (S O) n (fun i0 : nat => add i0 (add (mul i p) (S O)))) (add n (add (mul i p) (S O))))) (@nat2Zp p Hp (mul (@msum nat mul (S O) n (fun i : nat => add i (S O))) (add n (S O)))) *)
      do 2 rewrite nat2Zp_mult; f_equal; auto.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (add n (add (mul i p) (S O)))) (@nat2Zp p Hp (add n (S O))) *)
      apply nat2Zp_inj.
(* Goal: @eq nat (rem (add n (add (mul i p) (S O))) p) (rem (add n (S O)) p) *)
      rewrite (plus_comm n), <- plus_assoc, plus_comm.
(* Goal: @eq nat (rem (Nat.add (Nat.add (S O) n) (mul i p)) p) (rem (add n (S O)) p) *)
      rewrite <- rem_plus_div; auto.
(* Goal: @eq nat (rem (Nat.add (S O) n) p) (rem (add n (S O)) p) *)
      * f_equal; lia.
      * apply divides_mult, divides_refl.
  Qed.

  Notation φ := (fun n r => mprod_an (n*p+1) r).
  Notation Ψ := (fun n => Π n (fun i => mprod_an (i*p+1) (p-1))).

  Let phi_Zp_eq n r :〚φ n r〛=〚fact r〛.
  Proof. apply mprod_factorial_Zp. Qed.

  Fact mprod_factorial_mult n : fact (n*p) = expo n p * fact n * Ψ n.
  Proof.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i0 : nat => add i0 (add (mul i p) (S O))))) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i : nat => add i (S O)))) *)
    induction n as [ | n IHn ].
    + rewrite Nat.mul_0_l, msum_0, mscal_0, fact_0; auto.
    + replace (S n*p) with (n*p+p) by ring.
      rewrite mprod_factorial, msum_plus, <- mprod_factorial; auto.
      replace p with (S (p-1)) at 2 by omega.
(* Goal: @eq nat (fact (S n)) (@msum nat mul (S O) (S n) (fun i : nat => add i (S O))) *)
      rewrite msum_plus1; auto.
      rewrite <- plus_assoc.
      replace (p-1+1) with p by omega.
      replace (n*p+p) with ((S n)*p) by ring.
      rewrite mscal_S, fact_S, msum_S.
      rewrite IHn.
(* Goal: @eq nat (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k))) (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul p (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      repeat rewrite mult_assoc.
      rewrite (mult_comm _ p).
      repeat rewrite <- mult_assoc.
      do 2 f_equal.
      rewrite (mult_comm (S n)).
      repeat rewrite <- mult_assoc; f_equal.
      repeat rewrite mult_assoc; f_equal.
      rewrite msum_ext with (f := fun i => n*p+i+1)
                            (g := fun i => i+(n*p+1)).
      2: intros; ring. 
      rewrite <- msum_plus1; auto.
  Qed.
 
  Lemma mprod_factorial_euclid n r : fact (n*p+r) = expo n p * fact n * φ n r * Ψ n.
  Proof.
    rewrite mprod_factorial, msum_plus; auto.
    rewrite <- mprod_factorial.
    rewrite msum_ext with (f := fun i => n*p+i+1)
                          (g := fun i => i+(n*p+1)).
    2: intros; ring. 
    rewrite mprod_factorial_mult; auto; ring.
  Qed.

  Notation Zp := (Zp_zero Hp).
  Notation Op := (Zp_one Hp).
  Notation "∸" := (Zp_opp Hp).
  Infix "⊗" := (Zp_mult Hp) (at level 40, left associativity).
  Notation expoZp := (mscal (Zp_mult Hp) (Zp_one Hp)).

  Hint Resolve Nat_mult_monoid.

  Let Psi_Zp_eq n :〚Ψ n〛= expoZp n〚fact (p-1)〛.
  Proof.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i0 : nat => add i0 (add (mul i p) (S O))))) (@nat2Zp p Hp (@msum nat mul (S O) n (fun i : nat => add i (S O)))) *)
    induction n as [ | n IHn ].
    + rewrite msum_0, mscal_0; auto.
    + rewrite msum_plus1, nat2Zp_mult.
      rewrite mscal_plus1; auto.
      2: apply Zp_mult_monoid.
      2: apply Nat_mult_monoid.
      f_equal; auto.
  Qed.

  Hypothesis (Hprime : prime p).

  Let phi_Zp_invertible n r : r < p -> Zp_invertible Hp 〚φ n r〛.
  Proof.
(* Goal: forall _ : lt r p, @Zp_invertible p Hp (@nat2Zp p Hp ((fun n r : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i : nat => add i a)) (add (mul n p) (S O)) r) n r)) *)
    intros H; simpl; rewrite phi_Zp_eq.
(* Goal: @Zp_invertible p Hp (@nat2Zp p Hp (fact r)) *)
    apply Zp_invertible_factorial; auto.
  Qed.

  Let Psi_Zp_invertible n : Zp_invertible Hp 〚Ψ n〛.
  Proof.
(* Goal: @Zp_invertible p Hp (@nat2Zp p Hp ((fun n : nat => @msum nat mul (S O) n (fun i : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i0 : nat => add i0 a)) (add (mul i p) (S O)) (sub p (S O)))) n)) *)
    simpl; rewrite (Psi_Zp_eq n).
(* Goal: @Zp_invertible p Hp (@mscal (Z_Zp p) (@Zp_mult p Hp) (@Zp_one p Hp) n (@nat2Zp p Hp (fact (sub p (S O))))) *)
    apply Zp_expo_invertible, Zp_invertible_factorial; auto; omega.
  Qed.

  (** rewrite the binomial theorem

               fact k * fact (n-k) * binomial n k = fact n   

      when      

         k = K*p + k0
         n = N*p + n0

      with
       
      1)  K <= N & k0 <= n0
   
      we get n-k = (N-K)*p + (n0-k0) and

        expo K     p * fact K     * φ K      k0     * Ψ K
      .* expo (N-K) p * fact (N-K) * φ (N-K) (n0-k0) * Ψ (N-K)
      .* binomial n k 
      = expo N p     * fact N     * φ N      n0     * Ψ N.

      hence, simplifying by expo N p  we get

        fact K * fact (N-K) * φ K k0 * Ψ K * φ (N-K) (n0-k0) * Ψ (N-K) * binomial n k = fact N * φ N n0 * Ψ N. 

      then in Z/Zp we derive (modulo Wilson's theorem, unnecessary here〚fact (p-1)〛=〚-1〛) 

       〚fact K〛⊗〚fact (N-K)〛⊗〚fact k0〛⊗〚-1〛^K⊗〚fact (n0-k0)〛⊗〚-1〛^(N-K)⊗〚binomial n k〛
      =〚fact N〛⊗〚fact n0〛⊗〚-1〛^N

        that we combine with 〚fact K〛⊗〚fact (N-K)〛⊗〚binomial N K〛=〚fact N〛
                        and  〚fact k0〛⊗〚fact (n0-k0)〛⊗〚binomial n0 k0〛=〚fact n0〛

        to derive the result:〚binomial n k 〛=〚binomial N K〛⊗〚binomial n0 k0〛

      with 
 
      2) K < N & n0 < k0

      we have n-k = (N-(K+1))*p + (p-(k0-n0)) and

        expo K         p * fact K         * φ K          k0         * Ψ K
      .* expo (N-(K+1)) p * fact (N-(K+1)) * φ (N-(K+1)) (p-(k0-n0)) * Ψ (N-(K+1))
      .* binomial n k 
      = expo N p     * fact N     * φ N      n0     * Ψ N.

      hence
 
         fact K * φ K k0 * Ψ K * fact (N-(K+1)) * φ (N-(K+1)) (p-(k0-n0)) * Ψ (N-(K+1)) * binomial n k 
       = p * ....

      then in Z/Zp all the left factor are invertible except binomial n k which must thus be〚0〛 *)

  Section binomial_without_p_not_zero.

    Variable (n N n0 k K k0 : nat) (Hn : n = N*p+n0) (Hk : k = K*p+k0) (H1 : K <= N) (H2 : k0 <= n0).

    Let Hkn : k <= n.
    Proof.
(* Goal: le k n *)
      rewrite Hn, Hk.
      replace N with (K+(N-K)) by omega.
(* Goal: le (add (mul K p) k0) (add (mul (add K (sub N K)) p) n0) *)
      rewrite Nat.mul_add_distr_r.
      generalize ((N-K)*p); intros; omega.
    Qed.
   
    Let Hnk : n - k = (N-K)*p+(n0-k0).
    Proof.
(* Goal: @eq nat (sub n k) (add (mul (sub N K) p) (sub n0 k0)) *)
      rewrite Hn, Hk, Nat.mul_sub_distr_r.
      cut (K*p <= N*p).
      + generalize (K*p) (N*p); intros; omega.
      + apply mult_le_compat; auto.
    Qed.
  
    Fact binomial_wo_p : φ K k0 * Ψ K * φ (N-K) (n0-k0) * Ψ (N-K) * binomial n k 
                       = binomial N K * φ N n0 * Ψ N.
    Proof.
(* Goal: @eq nat (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k))) (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul p (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      apply (factorial_cancel (N-K)); repeat rewrite mult_assoc.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (fact K) (fact (sub N K))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub n0 k0) (fun i : nat => add i (add (mul (sub N K) p) (S O))))) (@msum nat mul (S O) (sub N K) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (Nat.mul (fact K) (binomial N K)) (fact (sub N K))) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite (mult_comm (fact _) (binomial _ _)).
(* Goal: @eq nat (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k))) (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul p (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      apply (factorial_cancel K); repeat rewrite mult_assoc.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (fact K) (fact (sub N K))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub n0 k0) (fun i : nat => add i (add (mul (sub N K) p) (S O))))) (@msum nat mul (S O) (sub N K) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (Nat.mul (fact K) (binomial N K)) (fact (sub N K))) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite (mult_comm (fact _) (binomial _ _)).
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (fact K) (fact (sub N K))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub n0 k0) (fun i : nat => add i (add (mul (sub N K) p) (S O))))) (@msum nat mul (S O) (sub N K) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (Nat.mul (binomial N K) (fact K)) (fact (sub N K))) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite <- binomial_thm; auto.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (fact K) (fact (sub N K))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub n0 k0) (fun i : nat => add i (add (mul (sub N K) p) (S O))))) (@msum nat mul (S O) (sub N K) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (fact N) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      apply expo_p_cancel with N.
(* Goal: @eq nat (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k))) (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul p (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      repeat rewrite mult_assoc.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) N p) (fact K)) (fact (sub N K))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub n0 k0) (fun i : nat => add i (add (mul (sub N K) p) (S O))))) (@msum nat mul (S O) (sub N K) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) N p) (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite <- mprod_factorial_euclid, <- Hn.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (fact n) *)
      rewrite binomial_thm with (1 := Hkn).
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (fact k)) (fact (sub n k))) *)
      rewrite Hnk. 
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (fact k)) (fact (add (mul (sub N (add K (S O))) p) (sub p (sub k0 n0))))) *)
      rewrite Hk at 3.
      replace N with (K+(N-K)) at 1 by omega.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (add K (sub N (add K (S O)))) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      rewrite power_plus.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (fact (add (mul K p) k0))) (fact (add (mul (sub N (add K (S O))) p) (sub p (sub k0 n0))))) *)
      do 2 rewrite mprod_factorial_euclid.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (mul (@mscal nat mul (S O) K p) (@mscal nat mul (S O) (sub N (add K (S O))) p)) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      ring.
    Qed.

    Hypothesis (Hn0 : n0 < p).

    Hint Resolve Zp_mult_monoid.

    Fact binomial_Zp_prod :〚binomial n k〛=〚binomial N K〛⊗〚binomial n0 k0〛.
    Proof.
      generalize binomial_wo_p; intros G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      apply f_equal with (f := nat2Zp Hp) in G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      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.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      repeat rewrite nat2Zp_mult in G.
      rewrite (Zp_mult_comm _ _〚 fact k0 〛) in G.
      repeat rewrite Zp_mult_assoc in G.
      rewrite (Zp_mult_comm _ _〚 fact k0 〛) in G.
      repeat rewrite <- Zp_mult_assoc in G.
      apply Zp_invertible_cancel_l in G.
      2: apply Zp_invertible_factorial; auto; omega.
      repeat rewrite Zp_mult_assoc in G.
      do 2 rewrite (Zp_mult_comm _ _〚 fact _ 〛) in G.
      repeat rewrite <- Zp_mult_assoc in G.
      apply Zp_invertible_cancel_l in G.
      2: apply Zp_invertible_factorial; auto; omega.
      repeat rewrite Zp_mult_assoc in G.
      rewrite <- mscal_plus in G; auto.
      replace (K+(N-K)) with N in G by omega.
      rewrite (Zp_mult_comm _ _ (expoZp _ _)) in G.
      apply Zp_invertible_cancel_l in G; trivial.
(* Goal: @Zp_invertible p Hp (@mscal (Z_Zp p) (@Zp_mult p Hp) (@Zp_one p Hp) n (@nat2Zp p Hp (fact (sub p (S O))))) *)
      apply Zp_expo_invertible, Zp_invertible_factorial; auto; omega.
    Qed.

  End binomial_without_p_not_zero.

  Section binomial_without_p_zero.

    Variable (n N n0 k K k0 : nat) (Hn : n = N*p+n0) (Hk : k = K*p+k0) 
             (H1 : K < N) (H2 : n0 < k0) (Hk0 : k0 < p).

    Let H3 : p - (k0-n0) < p.    Proof. omega. Qed.
    Let H4 : S (N-1) = N.        Proof. omega. Qed.
    Let H5 : N-1 = K+(N-(K+1)).  Proof. omega. Qed.
    Let H6 : N = K+1+(N-(K+1)).  Proof. omega. Qed.
    Let HNK : N-K = S (N-(K+1)). Proof. omega. Qed.

    Let Hkn : k <= n.
    Proof.
      rewrite Hn, Hk, H6.
(* Goal: le (add (mul K p) k0) (add (mul (add K (sub N K)) p) n0) *)
      do 2 rewrite Nat.mul_add_distr_r.
      generalize ((N-(K+1))*p); clear H3 H4 H5 H6 HNK; intros; omega.
    Qed.
   
    Let Hnk : n - k = (N-(K+1))*p+(p-(k0-n0)).
    Proof.
(* Goal: @eq nat (sub n k) (add (mul (sub N K) p) (sub n0 k0)) *)
      rewrite Hn, Hk, Nat.mul_sub_distr_r.
      cut ((K+1)*p <= N*p).
      + rewrite Nat.mul_add_distr_r.
        generalize (K*p) (N*p); clear H3 H4 H5 H6 HNK Hkn; intros; omega.
      + apply mult_le_compat; auto; clear H3 H4 H5 H6 HNK Hkn; omega.
    Qed.

    Fact binomial_with_p : fact K * fact (N-(K+1)) * φ K k0 * Ψ K * φ (N-(K+1)) (p-(k0-n0)) * Ψ (N-(K+1)) * binomial n k 
                         = p * fact N * φ N n0 * Ψ N.
    Proof.
(* Goal: @eq nat (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) ((fun n r : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i : nat => add i a)) (add (mul n p) (S O)) r) K k0)) ((fun n : nat => @msum nat mul (S O) n (fun i : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i0 : nat => add i0 a)) (add (mul i p) (S O)) (sub p (S O)))) K)) ((fun n r : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i : nat => add i a)) (add (mul n p) (S O)) r) (sub N (add K (S O))) (sub p (sub k0 n0)))) ((fun n : nat => @msum nat mul (S O) n (fun i : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i0 : nat => add i0 a)) (add (mul i p) (S O)) (sub p (S O)))) (sub N (add K (S O))))) (binomial n k)) (mul (mul (mul p (fact N)) ((fun n r : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i : nat => add i a)) (add (mul n p) (S O)) r) N n0)) ((fun n : nat => @msum nat mul (S O) n (fun i : nat => (fun a n0 : nat => @msum nat mul (S O) n0 (fun i0 : nat => add i0 a)) (add (mul i p) (S O)) (sub p (S O)))) N)) *)
      apply expo_p_cancel with (N-1).
(* Goal: @eq nat (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k))) (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul p (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      repeat rewrite mult_assoc.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) p) (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite (mult_comm (expo _ _) p).
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (Nat.mul p (@mscal nat mul (S O) (sub N (S O)) p)) (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite <- mscal_S.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (S (sub N (S O))) p) (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) *)
      rewrite H4, <- mprod_factorial_euclid, <- Hn.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (fact n) *)
      rewrite binomial_thm with (1 := Hkn).
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (fact k)) (fact (sub n k))) *)
      rewrite Hnk.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (fact k)) (fact (add (mul (sub N (add K (S O))) p) (sub p (sub k0 n0))))) *)
      rewrite Hk at 3.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (fact (add (mul K p) k0))) (fact (add (mul (sub N (add K (S O))) p) (sub p (sub k0 n0))))) *)
      do 2 rewrite mprod_factorial_euclid.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (sub N (S O)) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      rewrite H5 at 1.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (@mscal nat mul (S O) (add K (sub N (add K (S O)))) p) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      rewrite power_plus.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (mul (@mscal nat mul (S O) K p) (@mscal nat mul (S O) (sub N (add K (S O))) p)) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      ring.
    Qed.

    Fact binomial_with_p' : φ K k0 * Ψ K * φ (N-(K+1)) (p-(k0-n0)) * Ψ (N-(K+1)) * binomial n k 
                          = p * binomial N K * (N-K) * φ N n0 * Ψ N.
    Proof.
      apply (factorial_cancel (N-(K+1))); repeat rewrite mult_assoc.
(* Goal: @eq nat (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul (mul (mul (mul (fact K) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k))) (mul (@mscal nat mul (S O) (sub N (S O)) p) (mul (mul (mul p (fact N)) (@msum nat mul (S O) n0 (fun i : nat => add i (add (mul N p) (S O))))) (@msum nat mul (S O) N (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      apply (factorial_cancel K); repeat rewrite mult_assoc.
      rewrite binomial_with_p.
      rewrite binomial_thm with (n := N) (p := K).
      2: { apply lt_le_weak; auto. }
      rewrite HNK at 1.
      rewrite fact_S.
      rewrite <- HNK.
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (mul (@mscal nat mul (S O) K p) (@mscal nat mul (S O) (sub N (add K (S O))) p)) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      ring.
    Qed.
 
    Fact binomial_Zp_zero :〚binomial n k〛= Zp.
    Proof.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      generalize binomial_with_p'; intros G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      apply f_equal with (f := nat2Zp Hp) in G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      repeat rewrite nat2Zp_mult in G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      rewrite nat2Zp_p in G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      repeat rewrite Zp_mult_zero in G.
(* Goal: @eq (Z_Zp p) (@nat2Zp p Hp (binomial n k)) (@Zp_zero p Hp) *)
      apply Zp_invertible_eq_zero in G; auto.
(* Goal: @Zp_invertible p Hp (@Zp_mult p Hp (@Zp_mult p Hp (@Zp_mult p Hp (@nat2Zp p Hp (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@nat2Zp p Hp (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (@nat2Zp p Hp (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O)))))) (@nat2Zp p Hp (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
      repeat (apply Zp_mult_invertible; auto).
    Qed.

  End binomial_without_p_zero.

End fact.

Section lucas_lemma.

  (* https://math.stackexchange.com/questions/1463758/proof-of-lucas-theorem-without-the-polynomial-hint *)

  Variables (p : nat) (Hprime : prime p).

  Let Hp : p <> 0.
  Proof.
(* Goal: @eq nat (sub N K) (S (sub N (add K (S O)))) *)
    generalize (prime_ge_2 Hprime); intro; omega.
  Qed.

  Variables (n N n0 k K k0 : nat)
            (G1 : n = N*p+n0)  (G2 : n0 < p)
            (G3 : k = K*p+k0)  (G4 : k0 < p).

  Let choice : (K <= N  /\ k0 <= n0)
            \/ (n0 < k0 /\ K < N)
            \/ ((n0 < k0 \/ N < K) /\ n < k).
  Proof.
    destruct (le_lt_dec k n) as [ H0 | H0 ];
    destruct (le_lt_dec k0 n0) as [ H1 | H1 ];
(* Goal: @eq nat (sub N K) (S (sub N (add K (S O)))) *)
    destruct (le_lt_dec K N) as [ H2 | H2 ]; try omega.
    + do 2 right; split; auto.
(* Goal: lt n k *)
      rewrite G1, G3.
      replace K with (N+1+(K-N-1)) by omega.
(* Goal: le (add (mul K p) k0) (add (mul (add K (sub N K)) p) n0) *)
      do 2 rewrite Nat.mul_add_distr_r.
      generalize ((K-N-1)*p); intros; omega.
    + destruct (eq_nat_dec N K); try omega.
(* Goal: or (and (le K N) (le k0 n0)) (or (and (lt n0 k0) (lt K N)) (and (or (lt n0 k0) (lt N K)) (lt n k))) *)
      do 2 right; split; auto.
(* Goal: @eq nat (sub N K) (S (sub N (add K (S O)))) *)
      rewrite G1, G3; subst N; omega.
    + do 2 right; split; auto.
(* Goal: lt n k *)
      rewrite G1, G3.
      replace K with (N+1+(K-N-1)) by omega.
(* Goal: le (add (mul K p) k0) (add (mul (add K (sub N K)) p) n0) *)
      do 2 rewrite Nat.mul_add_distr_r.
      generalize ((K-N-1)*p); intros; omega.
  Qed.

  Theorem lucas_lemma : rem (binomial n k) p = rem (binomial N K * binomial n0 k0) p.
  Proof.
    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 ]; 
(* Goal: @eq nat (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (Nat.mul (mul (@mscal nat mul (S O) K p) (@mscal nat mul (S O) (sub N (add K (S O))) p)) (fact K)) (fact (sub N (add K (S O))))) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O)))))) (binomial n k)) (mul (mul (binomial n k) (mul (mul (mul (@mscal nat mul (S O) K p) (fact K)) (@msum nat mul (S O) k0 (fun i : nat => add i (add (mul K p) (S O))))) (@msum nat mul (S O) K (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) (mul (mul (mul (@mscal nat mul (S O) (sub N (add K (S O))) p) (fact (sub N (add K (S O))))) (@msum nat mul (S O) (sub p (sub k0 n0)) (fun i : nat => add i (add (mul (sub N (add K (S O))) p) (S O))))) (@msum nat mul (S O) (sub N (add K (S O))) (fun i : nat => @msum nat mul (S O) (sub p (S O)) (fun i0 : nat => add i0 (add (mul i p) (S O))))))) *)
           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.

End lucas_lemma.

Check lucas_lemma.
Print Assumptions lucas_lemma.
