proposition: Theorem Nbinomial_factorial : forall n k, 1 <= k -> k <= n -> (fact k) * Nbinomial n k = Nfinite_prod_0_n (pred k) (fun x => n - x).
proof: Proof. induction n. intros. destruct k. apply Nat.nle_succ_0 in H. contradiction. rewrite Nbinomial_outside. rewrite Nat.mul_0_r. assert (Nfinite_prod_0_n (pred (S k)) (fun x : nat => 0 - x) = Nfinite_prod_0_n (pred (S k)) (fun x : nat => 0)). apply Nfinite_prod_eq_compat. auto with arith. rewrite H1. clear H1. symmetry. apply Nfinite_prod_0_absord with k. auto with arith. reflexivity. auto with arith. intros. apply le_le_S_eq in H0. destruct H0. assert (Q: S k<=S n). exact H0. apply (Nat.le_trans k) in H0. destruct k. apply Nat.nle_succ_0 in H. contradiction. rewrite <- Nbinomial_pascal. rewrite Nat.mul_add_distr_l. apply le_le_S_eq in H. destruct H. apply le_le_S_eq in H0. destruct H0. rewrite IHn. unfold fact. fold fact. rewrite <- Nat.mul_assoc. rewrite IHn. assert (exists k', k=S k'). destruct k. apply Nat.nle_succ_diag_l in H. contradiction. exists k. reflexivity. destruct H1. rewrite H1. assert (pred (S(S x))=S(pred (S x))). rewrite <- Nat.sub_1_r. rewrite Nat.sub_succ_l. rewrite <- Nat.sub_1_r. reflexivity. auto with arith. rewrite H2. rewrite Nfinite_prod_split_upper. rewrite Nfinite_prod_split_lower. assert (Nfinite_prod_0_n (pred (S x)) (fun k0 : nat => S n - S k0) = Nfinite_prod_0_n (pred (S x)) (fun k0 : nat => n - k0)). apply Nfinite_prod_subtle_eq_compat. intros. auto with arith. rewrite H3. clear H3. assert (Nfinite_prod_0_n (pred (S x)) (fun x0 : nat => n - x0) * (n - S (pred (S x))) = (n - S (pred (S x))) * Nfinite_prod_0_n (pred (S x)) (fun x0 : nat => n - x0)). auto with arith. rewrite H3. clear H3. rewrite <- Nat.mul_add_distr_r. rewrite Nat.sub_0_r. assert (S (S x) + (n - S (pred (S x))) = S n). rewrite <- pred_Sn. assert (n-S x=S n-S(S x)). auto with arith. rewrite H3. rewrite Nat.add_comm. apply Nat.sub_add. rewrite <- H1. auto with arith. auto with arith. auto with arith. apply Nat.le_trans with (S k). auto with arith. auto with arith. auto with arith. auto with arith. assert (k=n). auto with arith. rewrite H1. rewrite Nbinomial_diag. rewrite Nbinomial_outside. rewrite Nat.mul_0_r. rewrite Nat.add_0_r. rewrite Nat.mul_1_r. rewrite Nfinite_prod_index_reversal. rewrite <- H1. rewrite Nfactorial_is_finite_prod. rewrite <- pred_Sn. apply Nfinite_prod_subtle_eq_compat. intros. assert (exists p, k=k0+p). apply Nle_plus. exact H2. destruct H3. rewrite Nat.add_comm in H3. rewrite H3. rewrite Nat.add_comm. assert (x-0=k0+x-(k0+0)). rewrite Nat.sub_0_r, Nat.add_0_r. rewrite Nat.add_comm. symmetry. rewrite Nat.add_sub; reflexivity. rewrite Nat.sub_0_r in H4. rewrite Nat.add_0_r in H4. rewrite <- H4. assert (S(k0+x)=S k0+x). auto with arith. rewrite H5. clear H4. clear H5. assert (S k0-0=x+S k0-(x+0)). rewrite Nat.sub_0_r, Nat.add_0_r. rewrite Nat.add_comm. symmetry. rewrite Nat.add_sub; reflexivity. rewrite Nat.add_0_r in H4. rewrite Nat.sub_0_r in H4. rewrite Nat.add_comm in H4. exact H4. auto with arith. assert (0=k). auto with arith. rewrite <- H1. unfold fact. unfold iter_nat. unfold pred. unfold Nfinite_prod_0_n. unfold Nbinomial. assert (leb 0 n=true). apply leb_correct. auto with arith. rewrite H2. clear H2. assert (leb 1 n=true). apply leb_correct. rewrite <- H1 in Q. auto with arith. rewrite H2. assert (Nbinomial n 0=1). apply Nbinomial_0. assert (Nbinomial n 1=n). apply Nbinomial_n_1. rewrite <- H1 in Q. auto with arith. unfold Nbinomial in H3. unfold Nbinomial in H4. rewrite H2 in H4. assert (leb 0 n=true). auto. rewrite H5 in H3. rewrite H3. rewrite H4. simpl. auto with arith. auto with arith. auto with arith. rewrite H0. rewrite Nbinomial_diag. rewrite <- pred_Sn. rewrite Nfactorial_is_finite_prod. rewrite Nfinite_prod_index_reversal. rewrite Nat.mul_1_r. apply Nfinite_prod_subtle_eq_compat. intros. symmetry. apply Nat.sub_succ_l. exact H1. Qed.
imports: Arith Compare Nfinite_prod Ndiv