# Theory Falling_Factorial_Sum_Combinatorics

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Proving Falling Factorial of a Sum with Combinatorics›

theory Falling_Factorial_Sum_Combinatorics
imports
Discrete_Summation.Factorials
Card_Partitions.Injectivity_Solver
begin

subsection ‹Preliminaries›

lemma card_lists_distinct_length_eq:
assumes "finite A"
shows "card {xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A} = ffact n (card A)"
proof cases
assume "n ≤ card A"
have "card {xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A} = ∏{card A - n + 1..card A}"
using ‹finite A› ‹n ≤ card A› by (rule card_lists_distinct_length_eq)
also have "… = ffact n (card A)"
using ‹n ≤ card A› by (simp add: prod_rev_ffact_nat'[symmetric])
finally show ?thesis .
next
assume "¬ n ≤ card A"
from this ‹finite A› have "∀xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A ⟶ False"
by (metis card_mono distinct_card)
from this have eq_empty: "{xs. length xs = n ∧ distinct xs ∧ set xs ⊆ A} = {}"
using ‹finite A› by auto
from ‹¬ n ≤ card A› show ?thesis
qed

subsection ‹Interleavings of Two Lists›

inductive interleavings :: "'a list ⇒ 'a list ⇒ 'a list ⇒ bool"
where
"interleavings [] ys ys"
| "interleavings xs [] xs"
| "interleavings xs ys zs ⟹ interleavings (x#xs) ys (x#zs)"
| "interleavings xs ys zs ⟹ interleavings xs (y#ys) (y#zs)"

lemma interleaving_Nil_implies_eq1:
assumes "interleavings xs ys zs"
assumes "xs = []"
shows "ys = zs"
using assms by (induct rule: interleavings.induct) auto

lemma interleaving_Nil_iff1:
"interleavings [] ys zs ⟷ (ys = zs)"
using interleaving_Nil_implies_eq1

lemma interleaving_Nil_implies_eq2:
assumes "interleavings xs ys zs"
assumes "ys = []"
shows "xs = zs"
using assms by (induct rule: interleavings.induct) auto

lemma interleaving_Nil_iff2:
"interleavings xs [] zs ⟷ (xs = zs)"
using interleaving_Nil_implies_eq2

lemma interleavings_Cons:
"{zs. interleavings (x#xs) (y#ys) zs} =
{x#zs|zs. interleavings xs (y#ys) zs} ∪ {y#zs|zs. interleavings (x#xs) ys zs}"
(is "?S = ?expr")
proof
show "?S ⊆ ?expr"
by (auto elim: interleavings.cases)
next
show "?expr ⊆ ?S"
by (auto intro: interleavings.intros)
qed

lemma interleavings_filter:
assumes "X ∩ Y = {}" "set zs ⊆ X ∪ Y"
shows "interleavings [z←zs . z ∈ X] [z←zs . z ∈ Y] zs"
using assms by (induct zs) (auto intro: interleavings.intros)

lemma interleavings_filter_eq1:
assumes "interleavings xs ys zs"
assumes "(∀x∈set xs. P x) ∧ (∀y∈set ys. ¬ P y)"
shows "filter P zs = xs"
using assms by (induct rule: interleavings.induct) auto

lemma interleavings_filter_eq2:
assumes "interleavings xs ys zs"
assumes "(∀x∈set xs. ¬ P x) ∧ (∀y∈set ys. P y)"
shows "filter P zs = ys"
using assms by (induct rule: interleavings.induct) auto

lemma interleavings_length:
assumes "interleavings xs ys zs"
shows "length xs + length ys = length zs"
using assms by (induct xs ys zs rule: interleavings.induct) auto

lemma interleavings_set:
assumes "interleavings xs ys zs"
shows "set xs ∪ set ys = set zs"
using assms by (induct xs ys zs rule: interleavings.induct) auto

lemma interleavings_distinct:
assumes "interleavings xs ys zs"
shows "distinct xs ∧ distinct ys ∧ set xs ∩ set ys = {} ⟷ distinct zs"
using assms interleavings_set by (induct xs ys zs rule: interleavings.induct) fastforce+

lemma two_mutual_lists_induction:
assumes "⋀ys. P [] ys"
assumes "⋀xs. P xs []"
assumes "⋀x xs y ys. P xs (y#ys) ⟹ P (x#xs) ys ⟹ P (x#xs) (y#ys)"
shows "P xs ys"
using assms by (induction_schema) (pat_completeness, lexicographic_order)

lemma finite_interleavings:
"finite {zs. interleavings xs ys zs}"
proof (induct xs ys rule: two_mutual_lists_induction)
case (1 ys)
show ?case by (simp add: interleaving_Nil_iff1)
next
case (2 xs)
then show ?case by (simp add: interleaving_Nil_iff2)
next
case (3 x xs y ys)
then show ?case by (simp add: interleavings_Cons)
qed

lemma card_interleavings:
assumes "set xs ∩ set ys = {}"
shows "card {zs. interleavings xs ys zs} = (length xs + length ys choose (length xs))"
using assms
proof (induct xs ys rule: two_mutual_lists_induction)
case (1 ys)
have "card {zs. interleavings [] ys zs} = card {ys}"
also have "… = (length [] + length ys choose (length []))" by simp
finally show ?case .
next
case (2 xs)
have "card {zs. interleavings xs [] zs} = card {xs}"
also have "… = (length xs + length [] choose (length xs))" by simp
finally show ?case .
next
case (3 x xs y ys)
have "card {zs. interleavings (x # xs) (y # ys) zs} =
card ({x#zs|zs. interleavings xs (y#ys) zs} ∪ {y#zs|zs. interleavings (x#xs) ys zs})"
also have "… = card {x#zs|zs. interleavings xs (y#ys) zs} + card {y#zs|zs. interleavings (x#xs) ys zs}"
proof -
have "finite {x # zs |zs. interleavings xs (y # ys) zs}"
moreover have "finite {y # zs |zs. interleavings (x # xs) ys zs}"
moreover have "{x # zs |zs. interleavings xs (y # ys) zs} ∩ {y # zs |zs. interleavings (x # xs) ys zs} = {}"
using ‹set (x # xs) ∩ set (y # ys) = {}› by auto
ultimately show ?thesis by (simp add: card_Un_disjoint)
qed
also have "… = card ((λzs. x # zs)  {zs. interleavings xs (y # ys) zs}) +
card ((λzs. y # zs)  {zs. interleavings (x#xs) ys zs})"
also have "… = card {zs. interleavings xs (y # ys) zs} + card {zs. interleavings (x#xs) ys zs}"
also have "… = (length xs + length (y # ys) choose length xs) + (length (x # xs) + length ys choose length (x # xs))"
using 3 by simp
also have "… = length (x # xs) + length (y # ys) choose length (x # xs)" by simp
finally show ?case .
qed

subsection ‹Cardinality of Distinct Fixed-Length Lists from a Union of Two Sets›

lemma lists_distinct_union_by_interleavings:
assumes "X ∩ Y = {}"
shows "{zs. length zs = n ∧ distinct zs ∧ set zs ⊆ X ∪ Y} = do {
k ← {0..n};
xs ← {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X};
ys ← {ys. length ys = n - k ∧ distinct ys ∧ set ys ⊆ Y};
{zs. interleavings xs ys zs}
}" (is "?S = ?expr")
proof
show "?S ⊆ ?expr"
proof
fix zs
assume "zs ∈ ?S"
from this have "length zs = n" and "distinct zs" and "set zs ⊆ X ∪ Y" by auto
define xs where "xs = filter (λz. z ∈ X) zs"
define ys where "ys = filter (λz. z ∈ Y) zs"
have eq: "[z←zs . z ∈ Y] = [z←zs . z ∉ X]"
using ‹set zs ⊆ X ∪ Y› ‹X ∩ Y = {}›
by (auto intro: filter_cong)
have "length xs ≤ n ∧ distinct xs ∧ set xs ⊆ X"
using ‹length zs = n› ‹distinct zs› unfolding xs_def by auto
moreover have "length ys = n - length xs"
using ‹set zs ⊆ X ∪ Y› ‹length zs = n›
unfolding xs_def ys_def eq
moreover have "distinct ys ∧ set ys ⊆ Y"
using ‹distinct zs› unfolding ys_def by auto
moreover have "interleavings xs ys zs"
using xs_def ys_def ‹X ∩ Y = {}› ‹set zs ⊆ X ∪ Y›
ultimately show "zs ∈ ?expr" by force
qed
next
show "?expr ⊆ ?S"
proof
fix zs
assume "zs ∈ ?expr"
from this obtain xs ys where "length xs ≤ n" "distinct xs" "set xs ⊆ X"
and "length ys = n - length xs" "distinct ys" "set ys ⊆ Y" "interleavings xs ys zs" by auto
have "length zs = n"
using ‹length xs ≤ n› ‹length ys = n - length xs› ‹interleavings xs ys zs›
using interleavings_length by force
moreover have "distinct zs"
using ‹distinct xs› ‹distinct ys› ‹interleavings xs ys zs› ‹set xs ⊆ X› ‹set ys ⊆ Y›
using ‹X ∩ Y = {}› interleavings_distinct by fastforce
moreover have "set zs ⊆ X ∪ Y"
using ‹interleavings xs ys zs› ‹set xs ⊆ X› ‹set ys ⊆ Y› interleavings_set by blast
ultimately show "zs ∈ ?S" by blast
qed
qed

lemma interleavings_inject:
assumes "(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}"
assumes "interleavings xs ys zs" "interleavings xs' ys' zs'"
assumes "zs = zs'"
shows "xs = xs'" and "ys = ys'"
proof -
have "xs = filter (λz. z ∈ set xs ∪ set xs') zs"
using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs ys zs›
by (auto intro: interleavings_filter_eq1[symmetric])
also have "… = filter (λz. z ∈ set xs ∪ set xs') zs'"
using ‹zs = zs'› by simp
also have "… = xs'"
using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs' ys' zs'›
by (auto intro: interleavings_filter_eq1)
finally show "xs = xs'" by simp
have "ys = filter (λz. z ∈ set ys ∪ set ys') zs"
using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs ys zs›
by (auto intro: interleavings_filter_eq2[symmetric])
also have "… = filter (λz. z ∈ set ys ∪ set ys') zs'"
using ‹zs = zs'› by simp
also have "… = ys'"
using ‹(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}› ‹interleavings xs' ys' zs'›
by (auto intro: interleavings_filter_eq2)
finally show "ys = ys'" .
qed

lemma injectivity:
assumes "X ∩ Y = {}"
assumes "k ∈ {0..n} ∧ k' ∈ {0..n}"
assumes "(length xs = k ∧ distinct xs ∧ set xs ⊆ X) ∧ (length xs' = k' ∧ distinct xs' ∧ set xs' ⊆ X)"
assumes "(length ys = n - k ∧ distinct ys ∧ set ys ⊆ Y) ∧ (length ys' = n - k' ∧ distinct ys' ∧ set ys' ⊆ Y)"
assumes "interleavings xs ys zs ∧ interleavings xs' ys' zs'"
assumes "zs = zs'"
shows "k = k'" and "xs = xs'" and "ys = ys'"
proof -
from assms(1,3,4) have "(set xs ∪ set xs') ∩ (set ys ∪ set ys') = {}" by blast
from this assms(5) ‹zs = zs'› show "xs = xs'" and "ys = ys'"
using interleavings_inject by fastforce+
from this assms(3) show "k = k'" by auto
qed

lemma card_lists_distinct_length_eq_union:
assumes "finite X" "finite Y" "X ∩ Y = {}"
shows "card {zs. length zs = n ∧ distinct zs ∧ set zs ⊆ X ∪ Y} =
(∑k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
(is "card ?S = _")
proof -
let ?expr = "do {
k ← {0..n};
xs ← {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X};
ys ← {ys. length ys = n - k ∧ distinct ys ∧ set ys ⊆ Y};
{zs. interleavings xs ys zs}
}"
from ‹X ∩ Y = {}› have "card ?S = card ?expr"
let "?S ⤜ ?comp" = "?expr"
{
fix k
assume "k ∈ ?S"
let "?expr" = "?comp k"
let "?S ⤜ ?comp" = "?expr"
from ‹finite X› have "finite ?S" by auto
moreover {
fix xs
assume xs: "xs ∈ ?S"
let ?expr = "?comp xs"
let "?S ⤜ ?comp" = ?expr
from ‹finite Y› have "finite ?S" by auto
moreover {
fix ys
assume ys: "ys ∈ ?S"
let ?expr = "?comp ys"
have "finite ?expr"
moreover have "card ?expr = (n choose k)"
using xs ys ‹X ∩ Y = {}› ‹k ∈ _›
by (subst card_interleavings) auto
ultimately have "finite ?expr ∧ card ?expr = (n choose k)" ..
}
moreover have "disjoint_family_on ?comp ?S"
using ‹k ∈ {0..n}› ‹xs ∈ {xs. length xs = k ∧ distinct xs ∧ set xs ⊆ X}›
by (injectivity_solver rule: injectivity(3)[OF ‹X ∩ Y = {}›])
moreover have "card ?S = ffact (n - k) (card Y)"
using ‹finite Y› by (simp add: card_lists_distinct_length_eq)
ultimately have "card ?expr = (n choose k) * ffact (n - k) (card Y)"
by (subst card_bind_constant) auto
moreover have "finite ?expr"
using ‹finite ?S› by (auto intro!: finite_bind finite_interleavings)
ultimately have "finite ?expr ∧ card ?expr = (n choose k) * ffact (n - k) (card Y)"
by blast
}
moreover have "disjoint_family_on ?comp ?S"
using ‹k ∈ {0..n}›
by (injectivity_solver rule: injectivity(2)[OF ‹X ∩ Y = {}›])
moreover have "card ?S = ffact k (card X)"
using ‹finite X› by (simp add: card_lists_distinct_length_eq)
ultimately have "card ?expr = (n choose k) * ffact k (card X) * ffact (n - k) (card Y)"
by (subst card_bind_constant) auto
moreover have "finite ?expr"
using ‹finite ?S› ‹finite Y› by (auto intro!: finite_bind finite_interleavings)
ultimately have "finite ?expr ∧ card ?expr = (n choose k) * ffact k (card X) * ffact (n - k) (card Y)"
by blast
}
moreover have "disjoint_family_on ?comp ?S"
by (injectivity_solver rule: injectivity(1)[OF ‹X ∩ Y = {}›])
ultimately have "card ?expr = (∑k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
from ‹card _ = card ?expr› this show ?thesis by simp
qed

lemma
"ffact n (x + y) = (∑k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
proof -
define X where "X = {..<x}"
define Y where "Y = {x..<x+y}"
have "finite X" and "card X = x" unfolding X_def by auto
have "finite Y" and "card Y = y" unfolding Y_def by auto
have "X ∩ Y = {}" unfolding X_def Y_def by auto
have "ffact n (x + y) = ffact n (card X + card Y)"
using ‹card X = x› ‹card Y = y› by simp
also have "… = ffact n (card (X ∪ Y))"
using ‹X ∩ Y = {}› ‹finite X› ‹finite Y› by (simp add: card_Un_disjoint)
also have "… = card {xs. length xs = n ∧ distinct xs ∧ set xs ⊆ X ∪ Y}"
using ‹finite X› ‹finite Y› by (simp add: card_lists_distinct_length_eq)
also have "… = (∑k=0..n. (n choose k) * ffact k (card X) * ffact (n - k) (card Y))"
using ‹X ∩ Y = {}› ‹finite X› ‹finite Y› by (simp add: card_lists_distinct_length_eq_union)
also have "… = (∑k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
using ‹card X = x› ‹card Y = y› by simp
finally show ?thesis .
qed

end


# Theory Falling_Factorial_Sum_Induction

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Proving Falling Factorial of a Sum with Induction›

theory Falling_Factorial_Sum_Induction
imports
Discrete_Summation.Factorials
begin

text ‹Note the potentially special copyright license condition of the following proof.›

"ffact n (x + y) = (∑k=0..n. (n choose k) * ffact k x * ffact (n - k) y)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
let ?s = "λk. (n choose k) * ffact k x * ffact (n - k) y"
let ?t = "λk. ffact k x * ffact (Suc n - k) y"
let ?u = "λk. ffact (Suc k) x * ffact (n - k) y"
have "ffact (Suc n) (x + y) = (x + y - n) * ffact n (x + y)"
also have "… = (x + y - n) * (∑k = 0..n. (n choose k) * ffact k x * ffact (n - k) y)"
using Suc.hyps by simp
also have "… = (∑k = 0..n. ?s k * (x + y - n))"
also have "… = (∑k = 0..n. ?s k * ((y + k - n) + (x - k)))"
proof -
have "?s k * (x + y - n) = ?s k * ((y + k - n) + (x - k))" for k
by (cases "k ≤ x ∨ n - k ≤ y") (auto simp add: ffact_nat_triv)
from this show ?thesis
by (auto intro: sum.cong simp only: refl)
qed
also have "… = (∑k = 0..n. (n choose k) * (?t k + ?u k))"
by (auto intro!: sum.cong simp add: Suc_diff_le ffact_Suc_rev_nat) algebra
also have "… = (∑k = 0..n. (n choose k) * ?t k) + (∑k = 0..n. (n choose k) * ?u k)"
also have "… = ?t 0 + (∑k = 0..n. (n choose k + (n choose Suc k)) * ?u k)"
proof -
have "… = (?t 0 + (∑k = 0..n. (n choose Suc k) * ?u k)) + (∑k = 0..n. (n choose k) * ?u k)"
proof -
have "(∑k = Suc 0..n. (n choose k) * ?t k) = (∑k = 0..n. (n choose Suc k) * ?u k)"
proof -
have "(∑k = Suc 0..n. (n choose k) * ?t k) = (∑k = Suc 0..Suc n. (n choose k) * ?t k)"
by simp
also have "… = (sum ((λk. (n choose k) * ?t k) o Suc) {0..n})"
by (simp only: sum.reindex[symmetric, of Suc] inj_Suc image_Suc_atLeastAtMost)
also have "… = (∑k = 0..n. (n choose Suc k) * ?u k)"
by simp
finally show ?thesis .
qed
from this show ?thesis
by (simp add: sum.atLeast_Suc_atMost[of _ _ "λk. (n choose k) * ?t k"])
qed
also have "… = ?t 0 + (∑k = 0..n. (n choose k + (n choose Suc k)) * ?u k)"
finally show ?thesis .
qed
also have "… = (∑k = 0..Suc n. (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
proof -
let ?v = "λk. (Suc n choose k) * ffact k x * ffact (Suc n - k) y"
have "… = ?v 0 + (∑k = 0..n. (Suc n choose (Suc k)) * ?u k)"
by simp
also have "… = ?v 0 + (∑k = Suc 0..Suc n. ?v k)"
by (simp only: sum.shift_bounds_cl_Suc_ivl diff_Suc_Suc mult.assoc)
also have "… = (∑k = 0..Suc n. (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
finally show ?thesis .
qed
finally show ?case .
qed

(* TODO: what's the right class here? *)
fixes x y :: "'a::{ab_group_add, comm_semiring_1_cancel, ring_1}"
shows "ffact n (x + y) = (∑k=0..n. of_nat (n choose k) * ffact k x * ffact (n - k) y)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
let ?s = "λk. of_nat (n choose k) * ffact k x * ffact (n - k) y"
let ?t = "λk. ffact k x * ffact (Suc n - k) y"
let ?u = "λk. ffact (Suc k) x * ffact (n - k) y"
have "ffact (Suc n) (x + y) = (x + y - of_nat n) * ffact n (x + y)"
also have "… = (x + y - of_nat n) * (∑k = 0..n. of_nat (n choose k) * ffact k x * ffact (n - k) y)"
using Suc.hyps by simp
also have "… = (∑k = 0..n. ?s k * (x + y - of_nat n))"
also have "… = (∑k = 0..n. ?s k * ((y + of_nat k - of_nat n) + (x - of_nat k)))"
also have "… = (∑k = 0..n. of_nat (n choose k) * (?t k + ?u k))"
proof -
{
fix k
assume "k ≤ n"
have "?u k = ffact k x * ffact (n - k) y * (x - of_nat k)"
by (simp add: ffact_Suc_rev Suc_diff_le of_nat_diff mult.commute mult.left_commute)
moreover from ‹k ≤ n› have "?t k = ffact k x * ffact (n - k) y * (y + of_nat k - of_nat n)"
by (simp add: ffact_Suc_rev Suc_diff_le of_nat_diff diff_diff_eq2 mult.commute mult.left_commute)
ultimately have
"?s k * ((y + of_nat k - of_nat n) + (x - of_nat k)) = of_nat (n choose k) * (?t k + ?u k)"
by (metis (no_types, lifting) distrib_left mult.assoc)
}
from this show ?thesis by (auto intro: sum.cong)
qed
also have "… = (∑k = 0..n. of_nat (n choose k) * ?t k) + (∑k = 0..n. of_nat (n choose k) * ?u k)"
by (simp add: sum.distrib distrib_left mult.commute mult.left_commute)
also have "… = ?t 0 + (∑k = 0..n. of_nat (n choose k + (n choose Suc k)) * ?u k)"
proof -
have "… = (?t 0 + (∑k = 0..n. of_nat (n choose Suc k) * ?u k)) + (∑k = 0..n. of_nat (n choose k) * ?u k)"
proof -
have "(∑k = Suc 0..n. of_nat (n choose k) * ?t k) = (∑k = 0..n. of_nat (n choose Suc k) * ?u k)"
proof -
have "(∑k = Suc 0..n. of_nat (n choose k) * ?t k) = (∑k = Suc 0..Suc n. of_nat (n choose k) * ?t k)"
also have "… = (sum ((λk. of_nat (n choose k) * ?t k) o Suc) {0..n})"
by (simp only: sum.reindex[symmetric, of Suc] inj_Suc image_Suc_atLeastAtMost)
also have "… = (∑k = 0..n. of_nat (n choose Suc k) * ?u k)"
by simp
finally show ?thesis .
qed
from this show ?thesis
by (simp add: sum.atLeast_Suc_atMost[of _ _ "λk. of_nat (n choose k) * ?t k"])
qed
also have "… = ?t 0 + (∑k = 0..n. of_nat (n choose k + (n choose Suc k)) * ?u k)"
finally show ?thesis .
qed
also have "… = (∑k = 0..Suc n. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
proof -
let ?v = "λk. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y"
have "… = ?v 0 + (∑k = 0..n. of_nat (Suc n choose (Suc k)) * ?u k)"
by simp
also have "… = ?v 0 + (∑k = Suc 0..Suc n. ?v k)"
by (simp only: sum.shift_bounds_cl_Suc_ivl diff_Suc_Suc mult.assoc)
also have "… = (∑k = 0..Suc n. of_nat (Suc n choose k) * ffact k x * ffact (Suc n - k) y)"
finally show ?thesis .
qed
finally show ?case .
qed

end

# Theory Falling_Factorial_Sum_Vandermonde

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Proving Falling Factorial of a Sum with Vandermonde Identity›

theory Falling_Factorial_Sum_Vandermonde
imports
"Discrete_Summation.Factorials"
begin

text ‹Note the potentially special copyright license condition of the following proof.›

shows "ffact k (n + m) = (∑i≤k. (k choose i) * ffact i n * ffact (k - i) m)"
proof -
have "ffact k (n + m) = fact k * ((n + m) choose k)"
by (simp only: ffact_eq_fact_mult_binomial)
also have "… = fact k * (∑i≤k. (n choose i) * (m choose (k - i)))"
by (simp only: vandermonde)
also have "… = (∑i≤k. fact k * (n choose i) * (m choose (k - i)))"
end