Library ssete7
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path div.
Require Import fintype tuple finfun bigop finset binomial.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma F7a n: 'C(n, 2) + 6 * 'C(n.+1, 4) = 'C(n, 2) ^ 2.
Proof.
case:n => // n; apply /eqP; rewrite - (eqn_pmul2l (ltn0Sn 3)); apply /eqP.
rewrite mulnDr - (expnMn 2 _ 2) - (mulnA 2 2) mulnCA - (mulnA 2 3).
rewrite - 2!mul_Sm_binm bin1 (mulnCA 3) - !mul_Sm_binm mulnCA.
rewrite (mulnCA 2) (mulnCA 2) (mulnCA n.+2) - mulnDr; case:n => //n.
rewrite - !mul_Sm_binm bin1 (mulnC _ n) mulnA - mulnDl - mulnn - mulnA.
by rewrite (mulnC n.+1) - {2} (add2n n) (mulSn _ n) addnA add2n - mulnS.
Qed.
Lemma binom_mn_n m n : 'C(m + n, m) = 'C(m + n, n).
Proof. by have:= (bin_sub (leq_addl m n)); rewrite addnK. Qed.
Lemma bin2' n: 'C(n.+1,2) * 2 = n * n.+1.
Proof. by rewrite mulnC -mul_Sm_binm bin1 mulnC. Qed.
Lemma mul_Sm_binm_1 n p: n * 'C(n+p,p) = p.+1 * 'C(n+p,p.+1).
Proof.
case: n => [| n]; first by rewrite add0n mul0n bin_small//.
rewrite -binom_mn_n addSn -mul_Sm_binm -mul_Sm_binm binom_mn_n //.
Qed.
Lemma mul_Sm_binm_r n k p: (n-k) ^_ p * 'C(n,k) = (k +p) ^_ p * 'C(n,k+p).
Proof.
move: k;elim:p => [k | p IHp k]; first by rewrite !ffactn0 addn0.
have aux: (n-k) * 'C(n,k) = k.+1 * 'C(n,k.+1).
case(leqP k n) => h; first by rewrite -{2 3}(subnK h) -mul_Sm_binm_1.
by rewrite bin_small // bin_small // ? muln0 // leqW.
rewrite 2!ffactnS (mulnC (n-k)) -mulnA aux mulnCA - subnS IHp {IHp}.
rewrite mulnA addnS -addSn; congr (_ * _).
case: p; [ by rewrite addn0 | move => p].
by rewrite ffactnS mulnCA addnS succnK ffactnSr addnK (mulnC _ k.+1).
Qed.
Lemma mul_Sm_binm_2 n k: (n-k) * 'C(n,k) = k.+1 * 'C(n,k.+1).
Proof. by have:= (mul_Sm_binm_r n k 1);rewrite !ffactn1 addn1. Qed.
Lemma binom_exchange j k q:
'C(j+k+q,j+k) * 'C(j+k,j) = 'C(k+q,k) * 'C(j+k+q,j).
Proof.
have bin_fact1: forall n m, 'C(n+m,m) * (m`! * n`!) = (n+m)`!.
by move => n m; move: (bin_fact (leq_addl n m)); rewrite addnK.
move: (bin_fact1 (k+q) j) (bin_fact1 q (j+k)).
rewrite (mulnC j`!) (addnC k)(addnC j) - (bin_fact1 q k) - (bin_fact1 k j).
rewrite (mulnAC _ _ j`!) !mulnA - (addnA q) (addnC q) => <-.
move /eqP; rewrite !eqn_pmul2r ? fact_gt0 //;move /eqP ->; apply: mulnC.
Qed.
Lemma binom_exchange1 j k n:
'C(j+n,j+k) * 'C(j+k,j) = 'C(n,k) * 'C(j+n,j).
Proof.
case: (ltnP n k) => nk; last by rewrite - (subnKC nk) addnA binom_exchange.
by rewrite (bin_small nk) bin_small ?mul0n // ltn_add2l.
Qed.
Lemma sum_bin_rec (n :nat) (f: nat -> nat):
\sum_(i<n.+1) 'C(n.+1,i.+1) * (f i) =
\sum_(i<n) 'C(n,i.+1) * (f i) + \sum_(i<n.+1) 'C(n,i) * (f i).
Proof.
transitivity
(\sum_(i < n.+1) 'C(n, i.+1) * (f i) + \sum_(i < n.+1) 'C(n, i) * (f i)).
rewrite - big_split; apply eq_bigr => // i _; rewrite binS mulnDl //.
by rewrite big_ord_recr /= bin_small ?addn0.
Qed.
Fixpoint der_rec n :=
if n is n'.+1 then if n' is n''.+1 then n' * (der_rec n'' + der_rec n')
else 0 else 1.
Definition derange n := nosimpl der_rec n.
Lemma derange0: derange 0 = 1. Proof. by []. Qed.
Lemma derange1: derange 1 = 0. Proof. by []. Qed.
Lemma derangeS n: derange n.+2 = (n.+1) * (derange n + derange n.+1).
Proof. by []. Qed.
Lemma derangeS1 n (p := n.+1 * derange n):
derange n.+1 = if (odd n) then p.+1 else p.-1.
Proof.
have pa: forall s, 0 <derange s.+2.
elim => // s dp; rewrite derangeS muln_gt0 ltn0Sn addn_gt0 dp orbT //.
have pn: forall s, ~~odd s -> 0 < (s.+1) * derange s.
by case => //;case => // s _; rewrite muln_gt0 ltn0Sn pa.
rewrite /p {p};elim :n => // n Hrec; rewrite derangeS Hrec /=.
move: (pn n); case (odd n).
move => _; rewrite /negb (mulSnr n.+1) [in X in _ = X] addnS succnK.
by rewrite - mulnDr (addnC).
by move => /= h; rewrite mulnDr; rewrite -{1} (@prednK (n.+1 * _)) // h.
Qed.
Lemma derange_sum n:
\sum_(i<n.+1) 'C(n,i) * (derange i) = n`! /\
\sum_(i<n.+1) 'C(n,i) * (derange i.+1) = n * n`!.
Proof.
elim:n => [| n [IH1 IH2]]; first by split; rewrite big_ord_recl big_ord0 //.
rewrite factS mulSn -IH2 -IH1;split.
rewrite (big_ord_recl n) big_ord_recl /= !bin0 mul1n -addnA; congr (_ + _).
exact: (sum_bin_rec n (fun i => (derange (i.+1)))).
rewrite -big_split big_distrr /= big_ord_recl add0n; apply: eq_bigr => i _.
by rewrite - mulnDr mulnA mul_Sm_binm derangeS mulnCA mulnA.
Qed.
Section Stirling.
Require Import fintype tuple finfun bigop finset binomial.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Lemma F7a n: 'C(n, 2) + 6 * 'C(n.+1, 4) = 'C(n, 2) ^ 2.
Proof.
case:n => // n; apply /eqP; rewrite - (eqn_pmul2l (ltn0Sn 3)); apply /eqP.
rewrite mulnDr - (expnMn 2 _ 2) - (mulnA 2 2) mulnCA - (mulnA 2 3).
rewrite - 2!mul_Sm_binm bin1 (mulnCA 3) - !mul_Sm_binm mulnCA.
rewrite (mulnCA 2) (mulnCA 2) (mulnCA n.+2) - mulnDr; case:n => //n.
rewrite - !mul_Sm_binm bin1 (mulnC _ n) mulnA - mulnDl - mulnn - mulnA.
by rewrite (mulnC n.+1) - {2} (add2n n) (mulSn _ n) addnA add2n - mulnS.
Qed.
Lemma binom_mn_n m n : 'C(m + n, m) = 'C(m + n, n).
Proof. by have:= (bin_sub (leq_addl m n)); rewrite addnK. Qed.
Lemma bin2' n: 'C(n.+1,2) * 2 = n * n.+1.
Proof. by rewrite mulnC -mul_Sm_binm bin1 mulnC. Qed.
Lemma mul_Sm_binm_1 n p: n * 'C(n+p,p) = p.+1 * 'C(n+p,p.+1).
Proof.
case: n => [| n]; first by rewrite add0n mul0n bin_small//.
rewrite -binom_mn_n addSn -mul_Sm_binm -mul_Sm_binm binom_mn_n //.
Qed.
Lemma mul_Sm_binm_r n k p: (n-k) ^_ p * 'C(n,k) = (k +p) ^_ p * 'C(n,k+p).
Proof.
move: k;elim:p => [k | p IHp k]; first by rewrite !ffactn0 addn0.
have aux: (n-k) * 'C(n,k) = k.+1 * 'C(n,k.+1).
case(leqP k n) => h; first by rewrite -{2 3}(subnK h) -mul_Sm_binm_1.
by rewrite bin_small // bin_small // ? muln0 // leqW.
rewrite 2!ffactnS (mulnC (n-k)) -mulnA aux mulnCA - subnS IHp {IHp}.
rewrite mulnA addnS -addSn; congr (_ * _).
case: p; [ by rewrite addn0 | move => p].
by rewrite ffactnS mulnCA addnS succnK ffactnSr addnK (mulnC _ k.+1).
Qed.
Lemma mul_Sm_binm_2 n k: (n-k) * 'C(n,k) = k.+1 * 'C(n,k.+1).
Proof. by have:= (mul_Sm_binm_r n k 1);rewrite !ffactn1 addn1. Qed.
Lemma binom_exchange j k q:
'C(j+k+q,j+k) * 'C(j+k,j) = 'C(k+q,k) * 'C(j+k+q,j).
Proof.
have bin_fact1: forall n m, 'C(n+m,m) * (m`! * n`!) = (n+m)`!.
by move => n m; move: (bin_fact (leq_addl n m)); rewrite addnK.
move: (bin_fact1 (k+q) j) (bin_fact1 q (j+k)).
rewrite (mulnC j`!) (addnC k)(addnC j) - (bin_fact1 q k) - (bin_fact1 k j).
rewrite (mulnAC _ _ j`!) !mulnA - (addnA q) (addnC q) => <-.
move /eqP; rewrite !eqn_pmul2r ? fact_gt0 //;move /eqP ->; apply: mulnC.
Qed.
Lemma binom_exchange1 j k n:
'C(j+n,j+k) * 'C(j+k,j) = 'C(n,k) * 'C(j+n,j).
Proof.
case: (ltnP n k) => nk; last by rewrite - (subnKC nk) addnA binom_exchange.
by rewrite (bin_small nk) bin_small ?mul0n // ltn_add2l.
Qed.
Lemma sum_bin_rec (n :nat) (f: nat -> nat):
\sum_(i<n.+1) 'C(n.+1,i.+1) * (f i) =
\sum_(i<n) 'C(n,i.+1) * (f i) + \sum_(i<n.+1) 'C(n,i) * (f i).
Proof.
transitivity
(\sum_(i < n.+1) 'C(n, i.+1) * (f i) + \sum_(i < n.+1) 'C(n, i) * (f i)).
rewrite - big_split; apply eq_bigr => // i _; rewrite binS mulnDl //.
by rewrite big_ord_recr /= bin_small ?addn0.
Qed.
Fixpoint der_rec n :=
if n is n'.+1 then if n' is n''.+1 then n' * (der_rec n'' + der_rec n')
else 0 else 1.
Definition derange n := nosimpl der_rec n.
Lemma derange0: derange 0 = 1. Proof. by []. Qed.
Lemma derange1: derange 1 = 0. Proof. by []. Qed.
Lemma derangeS n: derange n.+2 = (n.+1) * (derange n + derange n.+1).
Proof. by []. Qed.
Lemma derangeS1 n (p := n.+1 * derange n):
derange n.+1 = if (odd n) then p.+1 else p.-1.
Proof.
have pa: forall s, 0 <derange s.+2.
elim => // s dp; rewrite derangeS muln_gt0 ltn0Sn addn_gt0 dp orbT //.
have pn: forall s, ~~odd s -> 0 < (s.+1) * derange s.
by case => //;case => // s _; rewrite muln_gt0 ltn0Sn pa.
rewrite /p {p};elim :n => // n Hrec; rewrite derangeS Hrec /=.
move: (pn n); case (odd n).
move => _; rewrite /negb (mulSnr n.+1) [in X in _ = X] addnS succnK.
by rewrite - mulnDr (addnC).
by move => /= h; rewrite mulnDr; rewrite -{1} (@prednK (n.+1 * _)) // h.
Qed.
Lemma derange_sum n:
\sum_(i<n.+1) 'C(n,i) * (derange i) = n`! /\
\sum_(i<n.+1) 'C(n,i) * (derange i.+1) = n * n`!.
Proof.
elim:n => [| n [IH1 IH2]]; first by split; rewrite big_ord_recl big_ord0 //.
rewrite factS mulSn -IH2 -IH1;split.
rewrite (big_ord_recl n) big_ord_recl /= !bin0 mul1n -addnA; congr (_ + _).
exact: (sum_bin_rec n (fun i => (derange (i.+1)))).
rewrite -big_split big_distrr /= big_ord_recl add0n; apply: eq_bigr => i _.
by rewrite - mulnDr mulnA mul_Sm_binm derangeS mulnCA mulnA.
Qed.
Section Stirling.
Stirling Number of Second Kind
'St(n,m) is the number of partitions of a set of [n] elements into [p] parts
and 'St(n,m) is the number of surjective functions of a set with [n]
elements into a set with [p] elements.
Fixpoint stirling2_rec n m :=
match n, m with
| n'.+1, m'.+1 => m *stirling2_rec n' m + stirling2_rec n' m'
| 0, 0 => 1
| 0, _.+1 => 0
| _ .+1, 0 => 0
end.
Definition stirling2 := nosimpl stirling2_rec.
Definition nbsurj n m := (stirling2 n m) * m`!.
Notation "''St' ( n , m )" := (stirling2 n m)
(at level 8, format "''St' ( n , m )") : nat_scope.
Notation "''Sj' ( n , m )" := (nbsurj n m)
(at level 8, format "''Sj' ( n , m )") : nat_scope.
Lemma stirE : stirling2 = stirling2_rec. Proof. by []. Qed.
Lemma stir00 : 'St(0, 0) = 1. Proof. by []. Qed.
Lemma nbsurj00 : 'Sj(0, 0) = 1. Proof. by []. Qed.
Lemma stirn0 n : 'St(n.+1, 0) = 0. Proof. by []. Qed.
Lemma nbsurjn0 n : 'Sj(n.+1, 0) = 0. Proof. by []. Qed.
Lemma stir0n m : 'St(0, m.+1) = 0. Proof. by []. Qed.
Lemma nbsurj0n m : 'Sj(0, m.+1) = 0. Proof. by []. Qed.
Lemma stirS n m :
'St(n.+1, m.+1) = (m.+1) * 'St(n, m.+1) + 'St(n, m). Proof. by []. Qed.
Lemma nbsurjS n m : 'Sj(n.+1, m.+1) = (m.+1) * ('Sj(n, m.+1) + 'Sj(n, m)).
Proof.
by rewrite /nbsurj stirS mulnDr mulnDl - ! mulnA (mulnCA _ _ m`!) factS.
Qed.
Lemma stir_n1 n: 'St(n.+1, 1) = 1.
Proof. by elim: n => // n Ihn; rewrite stirS Ihn. Qed.
Lemma nbsurj_n1 n: 'Sj(n.+1, 1) = 1.
Proof. by rewrite /nbsurj stir_n1. Qed.
Lemma nbsurj_n2 n: 'Sj(n.+1, 2) = (2 ^n.+1 - 2).
Proof.
elim: n => // n Ihn; rewrite nbsurjS Ihn nbsurj_n1 (expnS _ n.+1).
rewrite -(subnK (leq_trans(_: 2 <= n.+2) (ltn_expl n.+1 (ltnSn 1)))) //.
by rewrite addnK 2!mulnDr (_: 2 * 2 = 2 +2) // addnA addnK.
Qed.
Lemma stir_n2 n: 'St(n.+1, 2) = (2 ^n - 1).
Proof.
elim: n => // n Ihn; rewrite stirS Ihn stir_n1 expnS.
rewrite -(subnK (leq_trans (ltn0Sn n) (ltn_expl n (ltnSn 1)))) //.
by rewrite addnK mulnDr (_: 2 * 1 = 1 + 1) // addnA addnK.
Qed.
Lemma stir_small n p: 'St(n, (n+p).+1) = 0.
Proof.
move: p; elim: n => [p // | n Hrec p].
by rewrite addSn stirS Hrec -addnS Hrec muln0.
Qed.
Lemma stir_small1 n p: n < p -> 'St(n,p) = 0.
Proof. by move /subnKC => <-; rewrite addSn stir_small. Qed.
Lemma nbsurj_small n p: 'Sj(n, (n+p).+1) = 0.
Proof. by rewrite /nbsurj stir_small1 // - addSn leq_addr. Qed.
Lemma stir_nn n: 'St(n, n) = 1.
Proof. by elim:n=> [//|n Hrec]; rewrite stirS Hrec stir_small1 ? muln0. Qed.
Lemma nbsurj_nn n: 'Sj(n, n) = n`!.
Proof. by rewrite /nbsurj stir_nn mul1n. Qed.
Lemma binn n : 'C(n, n) = 1.
Proof. by elim: n => [// |n IHn]; rewrite binS bin_small. Qed.
Lemma stir_Snn n: 'St(n.+1, n) = 'C(n.+1,2).
Proof.
elim:n => [//|n IHn].
by rewrite stirS IHn stir_nn muln1 addnC (binS (n.+1)) bin1.
Qed.
Lemma nbsurj_Snn n: 'Sj(n.+1, n) = 'C(n.+1,2) * n`!.
Proof. by rewrite /nbsurj stir_Snn. Qed.
Lemma stir_SSnn n: 'St(n.+2, n) = 'C(n.+3,4) + 2 * 'C(n.+2,4).
Proof.
elim:n => [// | n Hrec]; rewrite stirS Hrec stir_Snn addnCA (binS (n.+3)).
rewrite -addnA; congr (_ + _).
rewrite (binS (n.+2) 3) (addnC 'C(n.+2, 4)) mulnDr addnA; congr (_ + _).
by rewrite (binS (n.+2) 2) addnC addnA mulSnr -addn2 mul_Sm_binm_1 mulSnr.
Qed.
Lemma stir_Snn' n: 'St(n.+1, n) = \sum_(i<n.+1) i.
Proof.
elim: n => [//| n Ihn]; first by rewrite big_ord_recl big_ord0.
by rewrite big_ord_recr /= stirS Ihn stir_nn addnC muln1.
Qed.
Fixpoint euler_rec n m :=
match n, m with
| n'.+1, m'.+1 => m.+1 *euler_rec n' m + (n'-m') * euler_rec n' m'
| 0, _ => 0
| _.+1, 0 => 1
end.
Definition euler := nosimpl euler_rec.
Notation "''Eu' ( n , m )" := (euler n m)
(at level 8, format "''Eu' ( n , m )") : nat_scope.
Lemma eulerE : euler = euler_rec. Proof. by []. Qed.
Lemma euler0m m : 'Eu(0, m) = 0. Proof. by [] . Qed.
Lemma eulern0 n : 'Eu(n.+1, 0) = 1. Proof. by []. Qed.
Lemma eulerS n m : 'Eu(n.+1, m.+1) = m.+2 * 'Eu(n, m.+1) + (n-m) * 'Eu(n,m).
Proof. by []. Qed.
Lemma euler_small n p: 'Eu(n, n+p) = 0.
Proof.
move: p; elim: n => [p // | n Hrec p].
by rewrite addSn eulerS -addnS 2!Hrec 2!muln0.
Qed.
Lemma euler_small1 n p: n <= p -> 'Eu(n,p) = 0.
Proof. by move /subnKC => <-; rewrite euler_small. Qed.
Lemma euler_nn n: 'Eu(n.+1,n) = 1.
Proof.
elim :n => [// | n Hrec]; rewrite eulerS Hrec euler_small1 ?subSnn // muln0//.
Qed.
Lemma eulern1 n: 'Eu(n,1) + 'C(n.+1, 1) = 2 ^ n.
Proof.
elim:n => [// | n Hrec]; rewrite eulerS expnS - Hrec mulnDr - addnA {Hrec}.
by case: n => // n; rewrite eulern0 2!bin1 subn0 muln1 - addSnnS addnn -mul2n.
Qed.
Lemma eulern2 n: 'Eu(n,2) + 2^n * 'C(n.+1,1) = 3 ^n + 'C(n.+1, 2).
Proof.
elim:n => [// | n Hrec]; rewrite eulerS (binS n.+1 1).
apply /eqP; rewrite - (eqn_add2r (2 * 'C(n.+1, 2))); apply /eqP.
rewrite -3! addnA (addnAC _ 'C(n.+1, 1)) - mulSn (addnA (3 ^ n.+1))(expnS 3).
rewrite - mulnDr - Hrec {Hrec} mulnDr -addnA (mulnC 2) bin2'.
congr (_ + _);case: n => // n; rewrite subSS subn0 -{3} (bin1 n.+2) mulSnr.
rewrite (addnCA _ (n * _)) addnA - mulnDr eulern1 addnA.
rewrite mulnC (expnS _ n.+1) (mulnC 2) mulnAC - mulnA - mulnDr mulnCA !bin1.
by rewrite mulSn addnA addn2 - mulnS (mulnC 3).
Qed.
Lemma eulern3 n:
'Eu(n,3) + 3^n * (n.+1) + 'C(n.+1, 3) = 4 ^n + 2^n * 'C(n.+1, 2).
Proof.
elim:n => [// | n Hrec]; rewrite eulerS (binS n.+1 2) (addnC 'C(n.+1, 3)).
rewrite addnA - (addnA (4 * _)) - (addnA (4 * _)).
apply /eqP; rewrite - (eqn_add2r (4 * 3 ^ n * n.+1 + 3 * 'C(n.+1, 3))).
rewrite - addnA (addnCA 'C(n.+1, 3)) - addnA - mulSn - mulnA - mulnDr.
rewrite (addnC _ (4 * _)) addnA - mulnDr (addnA ('Eu( _,_))) Hrec {Hrec}.
rewrite mulnDr - expnS - mul_Sm_binm_2 mulnA - (mulnA 2 2) -expnS -mulnA.
rewrite mul2n -addnn (addnA (4 ^ n.+1)) (binS n.+1 1) mulnDr - 5!addnA.
apply /eqP; congr (_ + (_ + _)); case:n => // n; case :n => // n.
rewrite 4! subSS 2!subn0 expnS (mulnC 2) -mulnA (mulnC 2) bin2' -{1}(bin1 n.+3).
rewrite - {2} (addn2 n) mulnDl mulnDr mulnCA addnAC addnA - mulnDr.
rewrite (addnC _ 'Eu(n.+2, 2)) eulern2 addnC mulnA; congr (_ + _).
rewrite mulnDr addnAC addnA (expnS _ n.+2) mulnAC - mulnDl - addnA.
by rewrite - mulSn mulnS addnA addn3 - mulSn mulnAC mulnA.
Qed.
Lemma euler_sub n m: m <=n -> 'Eu(n.+1,m) = 'Eu(n.+1, n-m).
Proof.
move: m; elim: n; first by case.
move => n Hrec m; rewrite leq_eqVlt; move/orP; case.
by move /eqP => ->; rewrite euler_nn subnn eulern0.
rewrite ltnS; case: m; first by rewrite subn0 euler_nn eulern0.
move => m le1; rewrite (subSn le1) eulerS (eulerS n.+1) (subnSK le1).
rewrite addnC (subSn (ltnW le1)) (Hrec _ (ltnW le1)) (Hrec _ le1).
by rewrite (subSn (leq_subr _ _)) (subnBA _ le1) addKn.
Qed.
Lemma euler_sum n : \sum_(i<n.+1) 'Eu(n.+1,i) = (n.+1)`!.
Proof.
elim:n => [|n IHn]; first by rewrite big_ord_recl big_ord0 addn0.
rewrite big_ord_recl eulern0.
transitivity (1 + (\sum_(i < n.+1) (i.+2) * 'Eu(n.+1, lift ord0 i)
+ (\sum_(i < n.+1) (n.+1 -i) * 'Eu(n.+1, i)))).
congr (_ + _); rewrite -big_split /=; apply: eq_bigr => i _; apply: eulerS.
rewrite big_ord_recr big_ord_recl /= euler_small1 // muln0 addn0 muln1 subn0.
rewrite (addnCA _ n.+1) addnA add1n - big_split /= factS -IHn.
rewrite big_ord_recl eulern0 mulnDr muln1 big_distrr /=; congr (_ + _).
apply: eq_bigr; move => [i lin] _; rewrite -mulnDl /= (subSn lin).
by rewrite (subnSK lin) - add2n - addnA (addnC i) add2n subnK ? (ltnW lin).
Qed.
Lemma euler_sum_aux n p:
\sum_(i<n.+1) 'Eu(n.+1,i) * 'C(i,p) = 'Sj(n.+1, n.+1 - p).
Proof.
move:p; elim: n.
move => p; rewrite big_ord_recl big_ord0 /=; case p => //.
move => n Hrec p.
case (ltnP n.+1 p) => ltnp.
move : (ltnp); rewrite - subn_eq0 => /eqP ->; rewrite nbsurjn0 big1 //.
move => [i lin] _; rewrite bin_small //; apply: (leq_trans lin ltnp).
move: ltnp; case: p.
move => _; rewrite subn0 nbsurj_nn - euler_sum; apply: eq_bigr.
by move => i _; rewrite bin0 muln1.
move => p ltnp; rewrite (subSn ltnp) nbsurjS - Hrec subSS - {2} subSn //.
rewrite - Hrec - big_split big_distrr /= big_ord_recl add0n.
transitivity (\sum_(i < n.+1) (i.+2) * 'Eu(n.+1, i.+1) * 'C(i.+1, p.+1)
+ \sum_(i < n.+1) (n.+1-i) * 'Eu(n.+1, i) * 'C(i.+1, p.+1)).
rewrite - big_split /=; apply: eq_bigr => i _.
by rewrite - mulnDl - eulerS.
have ->: \sum_(i < n.+1) i.+2 * 'Eu(n.+1, i.+1) * 'C(i.+1, p.+1) =
\sum_(i < n.+1) i.+1 * 'Eu(n.+1, i) * 'C(i, p.+1).
rewrite big_ord_recr /= euler_small1 // muln0 addn0.
by symmetry; rewrite big_ord_recl /= add0n.
rewrite -big_split /=; apply: eq_bigr; move => [i lein] _ /=.
set x := 'Eu(n.+1, i).
rewrite 2! (mulnC _ x) -2! mulnA - 2! mulnDr (mulnCA _ x); congr (_ * _).
rewrite binS mulnDr addnA -mulnDl addSn subnKC ? (ltnW lein) //.
case (ltnP i p) => ltip.
by rewrite bin_small ? leqW // bin_small // 3!muln0.
rewrite mulnDr addnC {1} (_: (n - p).+1 = (n.+1 - i) + (i - p)).
by rewrite mulnDl mul_Sm_binm_2 -addnA -mulnDl addSn addnS subnKC.
by rewrite ltnS in lein; rewrite subSn // addSn - {1} (subnK lein) addnBA.
Qed.
Lemma euler_sum_pow k n : k ^n.+1 = \sum_(i<n.+1) 'Eu(n.+1,i) * 'C(k+i,n.+1).
Proof.
elim:n; first by rewrite big_ord_recl big_ord0 mul1n // addn0 bin1 //.
move => n Hrec.
rewrite big_ord_recl // addn0 eulern0 mul1n.
transitivity (\sum_(i < n.+2) i.+1 * 'Eu(n.+1, i) * 'C(k + i, n.+2)
+ (\sum_(i < n.+1) (n.+1-i) * 'Eu(n.+1, i) * 'C(k + i.+1, n.+2)));last first.
rewrite big_ord_recl // addn0 eulern0 mul1n - addnA -big_split /=.
by congr (_ + _); apply: eq_bigr => i _; rewrite -mulnDl -eulerS.
rewrite big_ord_recr /= euler_small1 // muln0 addn0 // -big_split /=.
rewrite expnS Hrec big_distrr /=; apply: eq_bigr => i _ /=.
rewrite mulnAC (mulnAC (n.+1 - i)) - mulnDl mulnC (mulnC _ 'Eu(_,_)).
rewrite addnS binS (mulnDr (n.+1 - i)) addnA - mulnDl addSn.
rewrite subnKC ?(@ltnW i) // -mul_Sm_binm_2 -mulnDl addnBA ? (@ltnW i) //.
case (ltnP (k + i) n.+1) => ltnp; first by rewrite (bin_small ltnp) !muln0.
by rewrite (subnK ltnp) addnK (mulnC k) mulnA.
Qed.
Lemma sum_pow_euler n k:
\sum_(i<n) i ^k.+1 = \sum_(i<k.+1) 'Eu(k.+1,i) * 'C(n+i,k.+2).
Proof.
move: k; elim :n.
move => k;rewrite big_ord0 big1 // => [] [i lin] _ /=.
by rewrite bin_small // add0n leqW //.
move => n IHn k; rewrite big_ord_recr /= IHn euler_sum_pow - big_split /=.
by apply: eq_bigr => i _; rewrite - mulnDr (addSn n) binS.
Qed.
Lemma F9aux2 n: \sum_(i<n) i ^5 =
'C(n, 6) + 26* 'C(n + 1, 6) + 66 * 'C(n + 2, 6) +
26 * 'C(n + 3, 6) + 'C(n + 4, 6).
Proof. rewrite sum_pow_euler 5! big_ord_recr /= big_ord0 2! mul1n addn0 //. Qed.
Section Partition.
Lemma neq_sym (T: eqType) (x y: T): (x != y) = (y != x).
Proof.
case: (_ =P _); first by move => ->; rewrite eqxx.
case: (_ =P _) => // -> //.
Qed.
Lemma disjointsU1 (T: finType) (A B: {set T}) x:
[disjoint (x |: A) & B] = (x \notin B) && [disjoint A & B].
Proof.
rewrite - !setI_eq0 setIUl; case h: (x \in B) => /=.
by apply /set0Pn; exists x; rewrite !inE h eqxx.
rewrite (_ : [set x] :&: B = set0) ? set0U //.
by apply /setP => y; rewrite !inE; apply /andP => [[/eqP ->]]; rewrite h.
Qed.
Lemma partition_ni_set0 (T:finType) (P: {set {set T}}) E i:
partition P E -> i \in P -> i != set0.
Proof.
by move /and3P => [_ _ /negP n0P]; apply:contraTneq => ->; apply /negP.
Qed.
Lemma card_partition_aux (T:finType) (P: {set {set T}}) E:
partition P E -> #|P| <= #|E|.
Proof.
move => pe;rewrite (card_partition pe) - sum1_card; apply: leq_sum => i.
rewrite card_gt0; apply: (partition_ni_set0 pe).
Qed.
Lemma partition_set0 (T:finType) (P: {set {set T}}) :
partition P set0 = (P == set0).
Proof.
apply /idP/eqP.
by move /card_partition_aux; rewrite cards0 leqn0 => /eqP /cards0_eq.
by move ->; rewrite /partition /trivIset /cover !big_set0 cards0 in_set0 !eqxx.
Qed.
Lemma card_inv_im (aT rT: finType) (f: aT -> rT) (A: {set aT}) (n: nat):
(forall x, x \in A -> #|[set y in A | f x == f y]| = n) ->
#|A| = #|f @: A| * n.
Proof.
pose g x := [set y in A | x == f y ].
have: {in f @: A &, injective g}.
move => x y /imsetP [x' x'A ->] /imsetP [y' y'A ->] => eq.
have: (x' \in (g (f x'))) by rewrite /g inE x'A eqxx.
by rewrite eq inE => /andP [_] /eqP.
move /imset_injP; rewrite -imset_comp; move /eqP => <- h.
apply:card_uniform_partition.
by move => a /imsetP [x xA ->]; rewrite - (h _ xA).
exact: preim_partitionP.
Qed.
Lemma stirling_partition (T: finType) (E: {set T}) (p:nat):
#|[set P | partition P E && (#|P| == p) ]| = 'St(#|E|, p).
Proof.
move: p; elim: {E} #|E| {1 3} E (refl_equal #|E|).
move => E /cards0_eq => ->; case.
apply: (eq_card1 (x := (@set0 (set_of_finType T)))) => p.
rewrite !inE cards_eq0 /= partition_set0; case : (p == set0) => //.
move => n;apply: eq_card0 => p; rewrite !inE partition_set0 -cards_eq0.
by apply /andP=> [[/eqP ->]].
move => n IHn E cE; case.
apply: eq_card0 => P; rewrite !inE; apply /andP => [[/and3P[/eqP cP p1 _ ]]].
by rewrite cards_eq0 => /eqP p2; move: p1; rewrite/trivIset cP cE p2 big_set0.
move => p.
move: (ltn0Sn n); rewrite -cE card_gt0 => /set0Pn [xa xaE].
move: (setD1K xaE); set E' := E :\ xa => eq1.
have xaE': xa \notin E' by rewrite !inE eqxx andFb.
move: (sym_eq (cardsU1 xa E')); rewrite eq1 cE xaE' addnC addn1.
move /eq_add_S => cE'; rewrite stirS - (IHn _ cE') - (IHn _ cE') {IHn}.
rewrite - sum1dep_card (bigID (fun P => (pblock P xa == [set xa]))) /=.
rewrite 2! sum1dep_card addnC; congr (_ + _).
pose f x := ((pblock x xa) :\ xa |: (x :\ (pblock x xa))).
set A := [set x | _]; set B := [set x | _].
have fAB: forall P (y := pblock P xa), P \in A ->
(((f P) \in B) /\
(xa \in y /\ (y \in P) /\ (y :\ xa \notin P :\ y))).
move => P y; rewrite !inE.
move => /andP [/andP [/and3P [/eqP cP /trivIsetP tI eP] /eqP sP] yxa].
have yP: y \in P by apply: pblock_mem; rewrite cP.
have xay: xa \in y by rewrite mem_pblock cP.
have yane: y :\ xa != set0.
apply: (contraNneq _ yxa); rewrite -/y -{2} (setD1K xay) => ->.
by rewrite setU0 eqxx.
have yanP: y :\ xa \notin P.
apply /negP => y'P; move: (tI _ _ y'P yP (proper_neq (properD1 xay))).
move /set0Pn: yane => [x /setD1P [xxa xy]] /pred0Pn.
by case;exists x; rewrite /= !inE // xxa xy.
have set0p: set0 \notin y :\ xa |: P :\ y.
by rewrite !inE negb_or neq_sym yane negb_and eP orbT.
have cy: cover (y :\ xa |: P :\ y) = E'.
move: cP; rewrite -{1} (setD1K yP) /cover 2!bigcup_setU 2! big_set1 /E'.
move => <-; apply /setP => x; rewrite in_setU 2! in_setD1 in_setU.
apply /idP /idP; last by case /andP => ->; rewrite andTb.
case /orP; first by move /andP => [-> ->] //.
move => h; rewrite h orbT andbT; apply: contraTneq h => ->.
rewrite /cover; apply/negP => /bigcupP [i] /setD1P [iy ip] xi.
by move /pred0P: (tI _ _ ip yP iy) => h;move: (h xa) => /=;rewrite xay xi.
have dia: forall s, s \in P :\ y -> y :\ xa != s -> [disjoint y :\ xa & s].
move => s /setD1P [sy sp] h1; move: (tI _ _ sp yP sy).
rewrite - setI_eq0 => /eqP hh; apply /pred0P => t /=.
by rewrite in_setD1 -andbA - in_setI setIC hh in_set0 andbF.
have tIy: trivIset (y :\ xa |: P :\ y).
apply /trivIsetP => s1 s2; case /setU1P => h1; case /setU1P => h2.
- by rewrite h1 h2 eqxx.
- by rewrite h1; apply: dia.
- by rewrite neq_sym disjoint_sym h2; apply: dia.
- by apply: tI; [ case /setD1P: h1 | case /setD1P: h2].
rewrite /partition set0p cy tIy eqxx 3!andTb.
by rewrite cardsU1 -sP (cardsD1 y P) yP in_setD1 negb_and yanP orbT.
pose g P y := ( xa |: y) |: (P :\ y).
have fBA: forall P y, P \in B -> y \in P -> (g P y) \in A /\ f (g P y) = P.
move => P y; rewrite !inE => /andP [/and3P [/eqP p1 p2 p3] /eqP p4] p5.
move /trivIsetP: (p2) => tI; rewrite /partition.
have xasP: forall s, s \in P -> xa \notin s.
move => s sP; apply: contra xaE'=> xas; rewrite -p1.
by apply /bigcupP; exists s.
move: (xasP _ p5) => xay.
have e1: (xa |: y \notin P :\ y).
by rewrite in_setD1 negb_and (contra (xasP _)) ?orbT // setU11.
have e2: xa |: y != [set xa].
by apply :contraNneq p3 => h; move: (setU1K xay); rewrite h setDv => ->.
have dia: forall s, s \in P :\ y -> xa |: y != s -> [disjoint xa |: y & s].
move => s /setD1P [sy sp] us; move: (tI _ _ sp p5 sy).
by rewrite disjointsU1 disjoint_sym (xasP _ sp) => ->.
have e3: trivIset (xa |: y |: P :\ y).
apply /trivIsetP => s1 s2; case /setU1P => h1; case /setU1P => h2.
- by rewrite h1 h2 eqxx.
- by rewrite h1; apply: dia.
- by rewrite h2 disjoint_sym neq_sym; apply: dia.
- by apply: tI; [ case /setD1P: h1 | case /setD1P: h2].
rewrite /g /f (def_pblock e3 (setU11 (xa |: y) (P :\ y))(setU11 xa y)).
rewrite in_setU1 negb_or in_setD1 negb_and p3 orbT neq_sym -card_gt0.
rewrite cardsU1 xay add1n ltn0Sn - p4 (cardsD1 y P) p5 cardsU1 e1 eqxx e2.
rewrite (setU1K xay) (setU1K e1) (setD1K p5) e3 !andbT - eq1 - p1.
by rewrite - {2} (setD1K p5) /cover 2!bigcup_setU 2! big_set1 setUA.
have -> : B = f @: A.
apply /setP => y; apply /idP/idP.
move => yb; move: (yb); rewrite inE => /andP [_] /eqP cy.
move: (ltn0Sn p); rewrite -cy card_gt0 => /set0Pn [x xy].
move: (fBA _ _ yb xy) => [h1 <-].
by apply /imsetP; exists (g y x).
move /imsetP => [P] pa ->; apply: (proj1 (fAB _ pa)).
rewrite mulnC; apply:card_inv_im => x xA.
move: (proj1 (fAB _ xA)); rewrite inE => /andP [_] /eqP => <-.
set s := [set y | _].
have ->: s = g (f x) @: f x.
apply /setP => t; rewrite inE; apply /idP/idP.
move => /andP [ta /eqP sf].
move: (fAB _ ta); set y := pblock t xa ; move => [pa [pb [pc pd]]].
apply /imsetP; exists (y :\ xa); first by rewrite sf;apply/setU1P; left.
by rewrite sf /f/g -/y (setD1K pb) (setU1K pd) (setD1K pc).
move /imsetP => [z zf ->];move: (fBA _ _ (proj1 (fAB _ xA)) zf).
by move => [-> ->]; rewrite eqxx.
move: (fAB _ xA); set y := pblock x xa ; move => [pa [pb [pc pd]]].
rewrite (card_in_imset) // => u v p1 p2 eq.
move: (fBA _ _ pa p1); rewrite inE => [][] /andP [] /andP [].
move /and3P => [_ tI _] _ _ _.
have p3 : pblock (g (f x) u) xa = xa |: u.
have r2: xa |: u \in (g (f x) u) by apply /setU1P; left.
by rewrite (def_pblock tI r2) // setU11.
have p4 : pblock (g (f x) v) xa = xa |: v.
rewrite eq in tI.
have r2: xa |: v \in (g (f x) v) by apply /setU1P; left.
by rewrite (def_pblock tI r2) // setU11.
have xau: forall u, u \in f x -> xa \notin u.
move: pa; rewrite inE => /andP [] /and3P [/eqP cf _ _] _.
move => w wf; apply/negP => xaw; move /negP:xaE'; rewrite -cf /cover.
by case; apply /bigcupP; exists w.
have ->: u = (xa |: u) :\ xa by rewrite setU1K //; apply: xau.
have ->: v = (xa |: v) :\ xa by rewrite setU1K //; apply: xau.
by rewrite -p3 -p4 eq.
have aux: forall P, partition P E' -> [set xa] \notin P.
move => P /and3P [] /eqP pa pb pc; apply /negP => pd.
move/negP: xaE'; case; rewrite -pa.
apply /bigcupP; exists [set xa] => //; apply: set11.
have h: {in [set P | partition P E' && (#|P| == p)] &,
injective (fun P => [set xa] |: P)}.
move => P Q; rewrite !inE => /andP [p1 _] /andP [p2 _] eq.
by rewrite - (setU1K (aux _ p1)) - (setU1K (aux _ p2)) eq.
rewrite -(card_in_imset h) {h}; apply: eq_card => y; rewrite !inE.
apply /idP/idP.
move /andP =>[] /andP [] /and3P [] /eqP uy ty ey /eqP cy /eqP uy'.
move: xaE; rewrite - uy => xay.
move: (pblock_mem xay); rewrite uy' => xsay; move: (setD1K xsay) => h.
apply /imsetP; exists (y :\ [set xa]) => //.
move: (cardsU1 [set xa] (y :\ [set xa])); rewrite h setD11 add1n cy => cy'.
rewrite inE -eqSS -cy' eqxx andbT /partition in_setD1 negb_and ey orbT andbT.
apply /andP; split.
rewrite /E' - uy - {2} h; rewrite /cover bigcup_setU big_set1 setU1K //.
apply /negP => /bigcupP => [] [i] /setD1P [iny iy] xai.
move /trivIsetP: ty => hh; move: (hh _ _ iy xsay iny).
by rewrite disjoint_sym disjoints_subset sub1set; move /setCP; case.
apply /trivIsetP => x x' /setD1P [] _ xy /setD1P [] _; move: xy.
move /trivIsetP: ty; apply.
move /imsetP => [x]; rewrite inE => /andP [px] /eqP cx -> {y}.
move /and3P: px => [] /eqP ux tx ex.
have pf: {in x, forall B : {set T}, [disjoint [set xa] & B]}.
move => s sy /=; rewrite (eq_disjoint1 (x:= xa)).
apply /negP => xas.
by move: xaE'; rewrite -ux; move /negP; case; apply /bigcupP; exists s.
by move => u; rewrite !inE.
move: (trivIsetU1 pf tx ex) => [qa qb].
rewrite /partition cardsU1 qa qb cx add1n.
rewrite (def_pblock qa (setU11 [set xa] x))? set11//.
rewrite /cover bigcup_setU big_set1 -/(cover x) ux eq1.
rewrite in_setU1 negb_or ex !eqxx ! andbT !andTb; apply /negP => /eqP h.
have // : 0 = 1 by rewrite - {1} (@cards0 T) h cards1.
Qed.
Lemma eqcard_equipotent (aT rT: finType):
(#|aT| = #|rT|) <-> (exists f : aT -> rT, bijective f).
Proof.
split.
move => sc.
move:(enum_val_bij aT) => []; set n1 := #|_ |; move => g1 c1 c2.
move:(enum_val_bij rT) => []; set n2 := #|_ |; move => g2 c3 c4.
have nn: n1 = n2 by rewrite /n1 /n2.
exists (fun x => enum_val (cast_ord nn (g1 x))).
exists (fun x => enum_val (cast_ord (sym_eq nn) (g2 x))).
by move => t /=;rewrite c3 cast_ord_comp cast_ord_id c2.
by move => t /=; rewrite c1 cast_ord_comp cast_ord_id c4.
move => [f bf].
have rtb: {on rT, bijective f} by apply: onW_bij.
rewrite -(on_card_preimset rtb) - cardsT.
have -> // : f @^-1: rT = [set: aT] by apply/setP=> x; rewrite !inE.
Qed.
Definition set_surj_fun_on (aT rT: finType) (B: {set rT}):=
[set f: {ffun aT -> rT} | f @: aT == B ].
Definition set_surj_fun (aT rT: finType):= set_surj_fun_on aT [set: rT].
Lemma set_surj_fun_onP (aT rT: finType)(B: {set rT} )(f: {ffun aT -> rT}):
reflect
((forall b, b \in B -> exists2 a, a \in aT & b = f a)
/\ (forall a, f a \in B))
(f \in set_surj_fun_on aT B).
Proof.
rewrite inE; apply: (iffP eqP).
move => <-; split;[ by move => b /imsetP | by move => a;apply: mem_imset].
move => [h1 h2]; apply /setP => b; apply /idP/idP.
move /imsetP => [x] _ ->;apply: h2.
by move => bb; apply /imsetP; apply: h1.
Qed.
Lemma set_surj_fun_P (aT rT: finType) (f: {ffun aT -> rT}):
reflect (forall b, exists a, b = f a)(f \in set_surj_fun aT rT).
Proof.
rewrite inE; apply: (iffP eqP) => h.
move => b; have brt: b \in f @: aT by rewrite h.
by move /imsetP: brt => [a _ ->]; exists a.
apply /setP => b; apply /idP/idP.
by move /imsetP; rewrite inE.
by move: (h b) => [a -> _]; apply: mem_imset.
Qed.
Lemma card_set_surj_fun_p1 (aT rT: finType) (B: {set rT}):
#|set_surj_fun_on aT B| = #|set_surj_fun aT (set_of_finType aT)|.
admit.
Qed.
Variables aT rT : finType.
Variables (f : aT -> rT).
End Partition.
Bell numbers
Definition Bell n := \sum_(i<n.+1) 'St(n, i).
Lemma Bell0: Bell 0 = 1.
Proof. by rewrite /Bell big_ord_recl big_ord0. Qed.
Lemma Bell1: Bell 1 = 1.
Proof. by rewrite /Bell 2!big_ord_recl big_ord0. Qed.
Definition br m p := \sum_(k<m.+1) 'C(m,k) * 'St(k,p).
Lemma foo1 n: br n n = 'St(n.+1,n.+1).
Proof.
rewrite /br big_ord_recr /= binn 2!stir_nn big1 // => i _.
by rewrite stir_small1.
Qed.
Lemma foo2 n: br n.+1 n = 'St(n.+2,n.+1).
Proof.
rewrite /br 2!big_ord_recr /= binn mul1n big1; last first.
by move => i _; rewrite stir_small1.
by rewrite add0n stirS binSn 2!stir_nn.
Qed.
Lemma foo3 n: br n.+2 n = 'St(n.+3,n.+1).
Proof.
rewrite /br 3!big_ord_recr /= binn mul1n big1; last first.
by move => i ; rewrite stir_small1.
rewrite add0n stirS binS binn mulnDl mul1n -addnA binSn stir_nn muln1.
rewrite addnA addnA stir_Snn (_: 'C(n.+2, n) + 'C(n.+1, 2) = n.+1 *n.+1).
rewrite - mulnDr stirS stir_nn muln1 stir_Snn //.
by rewrite -addn2 binom_mn_n addn2 binS addnAC addnn - muln2 bin2' bin1 mulSnr.
Qed.
Lemma Bell_rec n: Bell n.+1 = \sum_(k<n.+1) 'C(n,k) * Bell k.
Proof.
have aux: forall m p, \sum_(k<m.+1) 'C(m,k) * 'St(k,p) = 'St(m.+1,p.+1).
admit.
transitivity (\sum_(i < n.+1) \sum_(k < n.+1) 'C(n, k) * 'St(k, i)).
by rewrite /Bell big_ord_recl add0n; apply: eq_bigr =>i _; rewrite aux.
rewrite exchange_big /=; apply: eq_bigr; move=> [i lin ] _.
rewrite - big_distrr /= -(subnK lin) (addnC _ i.+1) big_split_ord /=.
by rewrite [X in (_ + X)] big1 ? addn0// => j _; rewrite stir_small1 ?leq_addr.
Qed.
Lemma nbsurj_SSnn n: nbsurj n.+2 n = ('C(n.+3,4) + 2 * 'C(n.+2,4)) * n`!.
Proof. by rewrite /nbsurj stir_SSnn. Qed.
Lemma sum_nbsurj n k: \sum_(i<k.+1) 'Sj(k,i) * 'C(n,i) = n ^k.
Proof.
move:n; elim:k; first by move => n; rewrite big_ord_recr big_ord0 nbsurj00 bin0.
move => k Hrec n; case:n.
by rewrite expnS mul0n big1 // => [] [i _] _ /=; case i.
move => n; rewrite expnS - Hrec big_ord_recl nbsurjn0 mul0n add0n.
transitivity (n.+1 * \sum_(i < k.+1) (('Sj(k, i) + 'Sj(k, i.+1)) * 'C(n, i))).
rewrite big_distrr; apply: eq_bigr; move => [i lik] _ //=.
by rewrite nbsurjS addnC mulnAC - mul_Sm_binm - mulnA (mulnC _ 'C(n, i)).
have aux: 'Sj(k, k.+1) = 0 by rewrite - [in k.+1] (addn0 k) nbsurj_small //.
congr (_ * _).
rewrite [x in _ = x] big_ord_recl bin0.
have ->: (\sum_(i < k) 'Sj(k, lift ord0 i) * 'C(n.+1, lift ord0 i) =
\sum_(i < k) 'Sj(k, lift ord0 i) * 'C(n, lift ord0 i)
+ \sum_(i < k.+1) 'Sj(k, lift ord0 i) * 'C(n, i) ).
rewrite [X in _ + X] big_ord_recr /= aux mul0n addn0 - big_split /=.
by apply: eq_bigr; move => i _; rewrite binS mulnDr.
rewrite addnA [X in _ = (X + _)] (_: _= \sum_(i < k.+1) 'Sj(k, i) * 'C(n, i)).
by rewrite - big_split; apply eq_bigr => i _; rewrite mulnDl.
by rewrite big_ord_recl bin0.
Qed.
Lemma sum_pow n k: \sum_(i<n) i ^k = \sum_(i<k.+1) 'Sj(k,i) * 'C(n,i.+1).
Proof.
elim:n => [| n Hrec]; first by rewrite big_ord0 big1 //.
rewrite big_ord_recr /= - sum_nbsurj Hrec - big_split //.
by apply: eq_bigr =>i _ /=; rewrite - mulnDr.
Qed.
Lemma F5aux n: \sum_(i<n) i = 'C(n,2).
Proof.
transitivity (\sum_(i<n) i ^1); first by apply:eq_bigr => //.
rewrite sum_pow ! big_ord_recr /= big_ord0 mul0n mul1n //.
Qed.
Lemma F5aux2 n: \sum_(i<n) i = 'C(n,2).
Proof.
by elim: n => [| n Hn]; [ rewrite big_ord0 | rewrite big_ord_recr Hn binS bin1].
Qed.
Lemma F6aux n: \sum_(i<n) i ^2 = 'C(n,2) + 2 * 'C(n,3).
Proof.
by rewrite sum_pow 3! big_ord_recr /= big_ord0 mul0n mul1n.
Qed.
Lemma n1bin n: n ^1 = 'C(n,1).
Proof. by rewrite bin1. Qed.
Lemma n2bin n: n ^2 = n * 'C(n,1).
Proof. by rewrite bin1. Qed.
Lemma n3bin n: n ^3 = 'C(n,1) + 6 * 'C(n.+1,3).
Proof.
rewrite -sum_nbsurj 4! big_ord_recr big_ord0 /= mul0n mul1n 2!add0n - addnA.
by rewrite - (mulnDr 6) binS (addnC 'C(n, 2)).
Qed.
Lemma n4bin n: n ^4 = n* 'C(n,1) + 6 * n*'C(n.+1,3) .
Proof. by rewrite (mulnC 6) - mulnA - mulnDr - n3bin expnS. Qed.
Lemma n5bin n: n ^5 = 'C(n,1) + 30 * 'C(n.+1,3) + 120 * 'C(n.+2,5).
Proof.
rewrite -sum_nbsurj 6! big_ord_recr big_ord0 /= mul0n mul1n 2!add0n.
rewrite (mulnDl 30 120) - 5!addnA (addnA (_ * 'C(n, 2))) -(mulnDr 30).
rewrite (addnC 'C(n, 2)) - binS -(mulnA 120 2) -2!(mulnDr 120).
congr (_ + (_ + (120 * _))).
by rewrite addnC 3!binS -2!addnA (addnA 'C(n,4)) addnn mul2n addnCA.
Qed.
Lemma n6bin n: n ^6 = n*'C(n,1) + 30 * n* 'C(n.+1,3) + 120 * n*'C(n.+2,5).
Proof.
by rewrite (mulnC 120) (mulnC 30) - 2! mulnA - 2!mulnDr - n5bin expnS.
Qed.
Lemma F7aux n: \sum_(i<n) i ^3 = 'C(n, 2) + 6 * 'C(n, 3) + 6 * 'C(n, 4).
Proof.
by rewrite sum_pow 4! big_ord_recr /= big_ord0 add0n nbsurjn0 mul0n add0n mul1n.
Qed.
Lemma F8aux n: \sum_(i<n) i ^4
= 'C(n, 2) + 14 * 'C(n, 3) + 36 * 'C(n, 4) + 24 * 'C(n, 5).
Proof.
by rewrite sum_pow 5! big_ord_recr /= big_ord0 mul0n mul1n.
Qed.
Lemma F9aux n: \sum_(i<n) i ^5 =
'C(n, 2) + 30 * 'C(n, 3) + 150 * 'C(n, 4) + 240 * 'C(n, 5)
+ 120 * 'C(n, 6).
Proof.
by rewrite sum_pow 6! big_ord_recr /= big_ord0 mul0n mul1n.
Qed.
Lemma F10aux n: \sum_(i<n) i ^6 =
'C(n, 2) + (31 *2) * 'C(n, 3) + (90 * 6) * 'C(n, 4) + (65 * 24) * 'C(n, 5)
+ (15 * 120) * 'C(n, 6) + 720 * 'C(n, 7).
Proof. by rewrite sum_pow 7! big_ord_recr /= big_ord0 mul0n mul1n. Qed.
Lemma F11aux n: \sum_(i<n) i ^7 =
'C(n, 2) + (63 * 2) * 'C(n, 3) + (301 * 3`!) * 'C(n, 4)
+ (350 * 4`!) * 'C(n, 5) + (140 * 5`!) * 'C(n, 6)
+ (21 * 6`!) * 'C(n, 7) + 7`! * 'C(n, 8).
Proof. by rewrite sum_pow 8! big_ord_recr /= big_ord0 mul0n mul1n. Qed.
Definition U_nkbin n k := 'C(n+k,k.*2.+2) + 'C((n+k).+1,k.*2.+2).
Definition T_nkbin n k := 'C(n+k,k.*2.+1) + 'C((n+k).+1,k.*2.+1).
Lemma UT_nkbin n k: T_nkbin n k.+1 + U_nkbin n.+1 k = T_nkbin n.+1 k.+1.
Proof.
rewrite /T_nkbin /U_nkbin !addSn ! addnS doubleS addnCA -addnA addnA -!binS.
by congr (_ + _); rewrite addnC - binS.
Qed.
Lemma U_nkbin_pr n k : n * 'C(n+k,k.*2.+1) = (k.+1) * (U_nkbin n k).
Proof.
rewrite /U_nkbin (binS _ k.*2.+1) addnA addnn mulnDr.
rewrite -(mul2n 'C(_,_)) mulnA mulSnr muln2 addn2 - mul_Sm_binm_2 - mulnDl.
rewrite - {2} addnn -addnS subnDA addnK -addnn - addSn.
by case (leqP k.+1 n) => h; rewrite ?(subnK h) // bin_small ? ltn_add2r ?muln0.
Qed.
Lemma T_nkbin_pr n k : n.*2.+1 * 'C(n+k,k.*2) = (k.*2.+1) * (T_nkbin n k).
Proof.
rewrite /T_nkbin binS addnA addnn - (muln2 'C(_, _)) mulnDr mulnA.
rewrite - mul_Sm_binm_2 (mulnC _ 2) mulnA - mulnDl addnS -{3} (mul2n k).
rewrite - mulnDr -(addnn k) subnDA addnK - mul2n.
case (leqP k n) => h; rewrite ?(subnK h) // bin_small ? ltn_add2r ?muln0 //.
Qed.
Lemma n2bin' n: n ^2 = U_nkbin n 0.
Proof. rewrite n2bin -(mul1n (U_nkbin n 0)) - U_nkbin_pr addn0 //. Qed.
Lemma n4bin' n: n ^4 = (U_nkbin n 0) + 12 * (U_nkbin n 1).
Proof.
rewrite n4bin -(mul1n (U_nkbin n 0)) -(mulnA 6 2) - 2! U_nkbin_pr.
by rewrite mulnA addn0 addn1.
Qed.
Lemma n6bin' n: n ^6 = (U_nkbin n 0) + 60* (U_nkbin n 1)+ 360 * (U_nkbin n 2).
Proof.
rewrite n6bin -(mul1n (U_nkbin n 0)) -(mulnA 30 2) -(mulnA 120 3).
by rewrite - 3! U_nkbin_pr 2! mulnA addn0 addn1 addn2.
Qed.
Lemma sn2bin n: \sum_(i<n.+1) i ^2 = T_nkbin n 1.
Proof.
by rewrite F6aux /T_nkbin mul2n - addnn addnCA (addnC 'C(n.+1, 2)) - binS addn1.
Qed.
Lemma sn4bin' n: \sum_(i<n.+1) i ^4 = (T_nkbin n 1) + 12 * (T_nkbin n 2).
Proof.
elim: n => [| n Hrec];first by rewrite big_ord_recl big_ord0 //.
rewrite big_ord_recr /= Hrec n4bin'.
by rewrite addnCA - addnA - mulnDr addnA (addnC (U_nkbin _ _)) 2!UT_nkbin.
Qed.
Lemma sn6bin' n:
\sum_(i<n.+1) i ^6 = (T_nkbin n 1) + 60 * (T_nkbin n 2) + 360 * (T_nkbin n 3).
Proof.
elim: n => [| n Hrec];first by rewrite big_ord_recl big_ord0 //.
rewrite big_ord_recr /= Hrec n6bin' addnCA - 2!addnA - mulnDr UT_nkbin.
rewrite (addnA ( _ * _)) (addnCA ( _ * _)) - mulnDr (addnC _ (T_nkbin n 2)).
by rewrite 2!addnA (addnC _ (T_nkbin n 1)) 2!UT_nkbin.
Qed.
End Stirling.
Lemma F1a n: \sum_(i<n) 1 = n.
Proof.
by rewrite big_const_ord //; elim:n => // h Hrec; rewrite iterS Hrec add1n.
Qed.
Lemma F1_aux n: \sum_(i<n) 1 = 'C(n,1).
Proof. by rewrite F1a bin1. Qed.
Lemma F5 n: (\sum_(i<n.+1) i) * 2 = n * (n.+1).
Proof. by rewrite F5aux bin2'. Qed.
Lemma F6 n: (\sum_(i<n.+1) i ^ 2 ) * 6 = n * (n.+1) * (2*n +1).
Proof.
elim: n; first by rewrite big_ord_recl big_ord0 //.
move => n Hrec;rewrite big_ord_recr /= mulnDl Hrec.
rewrite expnS expn1 (mulnC n) -!mulnA - mulnDr; congr (_ * _).
rewrite mulnDr muln1 - (add2n n) - (addn1 n) ! mulnDl mul1n.
rewrite 3!mulnDr (mulnA 2) (mulnC 4) -(addnA (n * 4)) (addnAC _ 6).
by rewrite addnA -mulnSr - 2!mulnDr addnCA - addnA addSnnS.
Qed.
Lemma F6' n: (\sum_(i<n.+1) i ^ 2 ) * 6 = n * (n.+1) * (n.*2.+1).
Proof.
rewrite F6aux mulnDl mulnAC (_: 2 * 6 = 4 * 3) // (_: 6 = 2 * 3) //.
rewrite mulnA bin2' - (mulnA 4) - mul_Sm_binm mulnCA (mulnC 4); case: n => // n.
rewrite (_: 4 = 2 * 2) // (mulnA _ 2) bin2' (mulnC n) -(mulnA _ n) mulnA.
by rewrite (mulnC n.+2) - mulnDr - muln2 (mulSn _ 2) addSn.
Qed.
Lemma F7 n: (\sum_(i<n.+1) i ^ 3 ) * 4 = (n * (n.+1)) ^2.
Proof.
elim: n; first by rewrite big_ord_recl big_ord0.
move => n Hrec;rewrite big_ord_recr /= mulnDl Hrec.
rewrite (expnD n.+1 2 1) mulnC 2 !expnMn expn1 -mulnA -mulnDr.
by rewrite - (addn2 n) sqrnD mulSn (mulnC 2) - mulnA -addnA.
Qed.
Lemma F7b n: (\sum_(i<n.+1) i ^ 3 ) = 'C(n.+1,2) ^2.
Proof. by rewrite F7aux - addnA - mulnDr (addnC 'C(n.+1, 3)) - binS F7a. Qed.
Lemma F8 n: (\sum_(i<n.+1) i ^ 4 ) * 30 =
n * (n.+1) * (n.*2.+1) * (3*n*n + 3*n -1).
Proof.
have pa: (24 * 30 = (36 * 4) *5) by done.
have pb: (36 * 30 = (90 * 3) *4) by done.
have pc: (14 * 30 = (70 * 2) *3) by done.
have pd: (30 = 2 * 15) by done.
rewrite F8aux 3! mulnDl mulnAC pc (mulnAC 36) pb (mulnAC 24) pa {1} pd.
rewrite - (mulnA _ 3) - (mulnA _ 4) - (mulnA _ 5) - 3! mul_Sm_binm.
rewrite (mulnCA (_ *4)) (mulnCA (90 * 3)) (mulnCA (70 * 2)) (mulnA _ 2) bin2'.
rewrite (mulnC n) - mulnA - 3! mulnDr -5!mulnA; congr (_ * _); case:n => //n.
rewrite - 3! mul_Sm_binm (mulnCA 70) (mulnCA 90) (mulnCA 36) - 3! mulnDr.
congr (_ * _); case:n => // n.
rewrite bin1 (_: 90 = 45 *2) // [in 36 * _] (_: 36 = (6 * 2) * 3) //.
rewrite - (mulnA _ 2) - (mulnA _ 3) - 2! mul_Sm_binm bin1 (mulnCA (6 * 2)).
case:n => // n;rewrite - (mulnA 6) -mul_Sm_binm bin1 mulnCA -addnA -mulnDr.
rewrite (mulnC _ n) (mulnA 6) - mulnDl mulnCA.
rewrite -(addnA 24) (addnC 21) (mulnAC 2 3) - (mulnDl (2 * n) 7 3).
rewrite mulnDl addnA (mulnC n.+2) (mulnA 24) - (addnA 15) - mulnDl.
rewrite (mulnS 24) addnA -(addnA 10 84) (mulnAC 2 12) (addnC 84).
rewrite - (mulnDl (2 * n) 7) mulnDl addnA (addnC 15) 2!mulnSr.
rewrite (mulnAC 2 5) - (addnA _ _ 15) - (addnA _ 10) - (mulnDl (2 * n) 7 5).
rewrite - mulnA - mulnA - 2! mulnDr; congr (_ * _).
by rewrite addnS - mul2n 3!mulnSr - 2!addnA //.
rewrite {2} (mulnSr 3) addnA (addnS _ 2) subn1 (succnK) -mulnA - addnA.
rewrite - (addnA 2 (3 * 1)) - (mulnA 3 4) - 3!mulnDr addnC.
rewrite (mulnDl 2 2) - addnA -mulnDl add2n mul2n -addnn addnA addnCA.
by rewrite add1n -addnA - mulnS (addnC _ n.+2).
Qed.
Lemma F9 n: (\sum_(i<n.+1) i ^ 5 ) * 12 =
n * n * (n.+1) * (n.+1) * (2*n*n + 2*n -1).
Proof.
have pa: (120 * 12 = (48 * 5) *6) by done.
have pb: (240 * 12 = (144 * 4) *5) by done.
have pc: (150 * 12 = (150 * 3) *4) by done.
have pd: (30 * 12 = (60 * 2) *3) by done.
have pe: (12 = 2 * 6) by done.
rewrite F9aux 4!mulnDl mulnAC pd (mulnAC 150) pc (mulnAC 240) pb.
rewrite (mulnAC 120) pa {1} pe (mulnA _ 2) bin2' - (mulnA _ 3) - (mulnA _ 4).
rewrite - (mulnA _ 5) - (mulnA _ 6) - 4! mul_Sm_binm {pa pb pc pd pe}.
rewrite (mulnCA (_ *5)) (mulnCA (_ * 4)) (mulnCA (_ * 3)) (mulnCA (60 * 2)).
rewrite (mulnC n) - mulnA - 4! mulnDr (mulnAC n n) (mulnC n n.+1) - 7!mulnA.
congr (_ * _); case:n => // n; rewrite - 4! mul_Sm_binm.
rewrite (mulnCA 60) (mulnCA 150) (mulnCA 144) (mulnCA 48) - 4! mulnDr.
rewrite {2} (mulnSr 2 n) (addnA _ 1 1) addnA addnK -3 !addnA.
have ->: (2 * n.+1 * n.+1 + (2 * n + 1)) = (2* n +6) *n +3.
rewrite - mulnA mulnSr mulnDr mulnA mulnSr addnA addnAC - (addnA _ _ 1).
by rewrite addnAC - mulnDl -2!addnA addnA - mulnDl -addnA.
have ->: n.+1 * (n.+2 * ((2 * n + 6) * n + 3)) =
6 + n * (n.+1 * (n.+2) * (2*n +6) + 3* (n+3)).
rewrite 3!mulnDr 3!mulnA mulnC addnCA (mulnCA _ 3) - (mulnDr 3 2).
by rewrite (mulnC 3) {2} mulSn -{2} add2n -{2} addn2 -(addnA 2) -mulnS -addnS.
congr (_ * (6 + _)); case:n => // n.
have ->: n.+2 * n.+3 * (2 * n.+1 + 6) + 3 * (n.+1 + 3) =
60 + n * (2*n*n + 18 * n + 55 ).
rewrite (addSn n 3) - addnS (mulnDr 3) addnA (mulnSr 2 n) -(addnA _ 2).
rewrite mulnDr - {3} (addn2 n) mulnDl - {3} (addn3 n) (mulnDr 2).
rewrite (mulnC 2) addnA - mulnDr mulnDl addnA mulnC - 2!mulnA.
rewrite - mulnDr addnAC addnC -addnA addnA mulnC - mulnDr addnC.
congr (60 + (n * _)); rewrite - (addn3 n) - addnA mulnDl (mulnC n 8).
rewrite -(addn2 n) mulnA mulnDr (mulnAC 2 _ 3) (mulnDr 6) addnC.
rewrite (addnA _ (6 * n)) -mulnDl mulnDr (addnCA _ _ 40) 2!addnA.
by rewrite -2!mulnDl -3!addnA (addnCA 8) (mulnC 2).
rewrite - (mulnA 75 2) - (mulnA 12 4) - (mulnA 48 3) - 3! mul_Sm_binm bin1.
rewrite mulnC (mulnCA 75) (mulnCA 48) (mulnCA 12) - 3! mulnDr.
congr (_ * (60 + _)).
case:n => // n; rewrite - (mulnA 24 2) - (mulnA 4 3) - 2! mul_Sm_binm bin1.
rewrite mulnCA (mulnCA 4) mulnC - 2!mulnDr; congr (_ * _).
transitivity (75 +((22 + 2 * n) * n)).
congr (_ + _); case:n => //n; rewrite - (mulnA 2 2) - mul_Sm_binm !bin1.
by rewrite (mulnC _ n) mulnA -mulnDl - (addnA 22 2) (mulnS 2 n).
rewrite (mulnSr 18 n) - 2!addnA addnCA addnA 2! mulnSr (addnA (18 * n)).
rewrite -mulnDl {1} (addnC _ 2) (addnA 18) (addnA _ _ 2) -mulnDl.
by rewrite -addnA addnC addnAC.
Qed.
Lemma F9' n (a := 'C(n.+1,2)): (\sum_(i<n.+1) i ^ 5 ) * 3 = a * a * (4*a -1).
Proof.
apply /eqP; rewrite - (eqn_pmul2r (ltn0Sn 3)) - mulnA F9; apply /eqP.
rewrite (mulnAC n) - (mulnA _ n) - mulnDl - mulnSr - (mulnA 2).
rewrite (mulnC _ n) - bin2' -/a (mulnC _ 2) (mulnA 2 2) (mulnC _ 4).
by rewrite - (mulnA 2) (mulnCA a 2) mulnA - mulnA.
Qed.
Lemma F12 n: \sum_(i<n) (i.*2.+1) = n ^2.
Proof.
elim: n; first by rewrite big_ord0.
move => n Hrec;rewrite big_ord_recr /= Hrec.
rewrite - (addn1 n) sqrnD -addnA; congr (_ + _).
by rewrite muln1 mulnC add1n muln2.
Qed.
Lemma F13' n: \sum_(i<n) (i.*2.+1)^2 = 8 * 'C(n.+1,3) + 'C(n,1).
Proof.
elim :n => //; first by rewrite big_ord0 bin0n.
move => n Hrec; rewrite big_ord_recr Hrec /= (binS (n.+1)) mulnDr !bin1.
rewrite addnAC -{4} (add1n n) addnA - (addnA _ _ 1); congr (_ + _ + _).
rewrite -(mulnA 4 2) -mul_Sm_binm bin1 -addn1 sqrnD - !mulnn !muln1 addnAC.
by rewrite - mulnDl mulnA (mulnAC 2 2) - mulnA (mul2n n) mulnSr mul2n.
Qed.
Lemma F13 n: (\sum_(i<n) (i.*2.+1)^2) * 3 = n * (n ^2 * 4 - 1).
Proof.
rewrite F13'; case: n => //n.
rewrite bin1 mulnDl mulnAC - mulnA - mul_Sm_binm (mulnC n.+2).
rewrite - (mulnA 4 2) (mulnA 2) - mul_Sm_binm bin1 -mulnA (mulnC 4) - mulnA.
rewrite - mulnDr; congr (_ * _); rewrite -addn1 mulnDr mulnDl muln1.
by rewrite - mulnn mulSnr mulnDl (mulSnr n 4) (addnA _ 3 1) !addnA addnK.
Qed.
Lemma F13direct n: (\sum_(i<n) ((i*2).+1)^2) * 3 = n * (n ^2 * 4 - 1).
Proof.
elim: n; first by rewrite big_ord0.
move => n Hrec;rewrite big_ord_recr /= mulnDl Hrec {Hrec}.
have aux: forall m, (m.+1) ^2 *4 - 1 = m^2 *4 + m * 8 + 3.
move => m; rewrite -(addn1 m) sqrnD muln1 exp1n mulnDl.
rewrite mulnDl mul1n - mulnAC addnAC - (mulnC m) (_ : 2 * 4 = 8) //.
by rewrite -(addn1 3) addnA addn1 subn1 -pred_Sn.
have aux2: forall m, (m ^2) *4 -1 = ((m * 2).+1) * ( (m * 2).-1).
case => [// | m].
rewrite aux - (addn1 m) mulnDl mul1n - addnS addn2 -pred_Sn -(addn1 (m*2)).
rewrite mulnDl (mulnC 3) mulnDr mulnDl mulnAC // addnA.
congr (_ + _);rewrite - addnA ; congr (_ + _); rewrite -!mulnA //- mulnDr.
done.
have aux3: forall m, (m.+1 * 2).-1 = (m* 2).+1.
by move => m;rewrite -(addn1 m) mulnDl mul1n addn2 -pred_Sn.
rewrite aux2 aux2 aux3.
rewrite mulnCA expnS expn1 -mulnA - mulnDr.
symmetry; rewrite mulnA mulnC; congr(_ * _).
case: n => [// | n].
rewrite aux3.
have ->: (n.+1 * 2).+1 * 3 = (1* (n * 2).+1) + n*4 + 8.
rewrite mul1n -(addn1 n) mulnDl -addnS mulnDl mul1n.
rewrite - (addn1 (n * 2)) addnAC -addnA -addnA (addnA 1 8) add1n.
by rewrite addnCA - mulnDr addnC -mulnA.
symmetry; rewrite addnA addnA -mulnDl addn1 -addnA.
have ->: (n * 4 + 8) = n.+2 * 4 by rewrite -(addn2 n) mulnDl.
rewrite -mulnDr; congr (_ * _).
by rewrite addSn - (addn2 n) mulnDl.
Qed.
Fixpoint cfn2_rec n m :=
match n, m with
| n'.+1, m'.+1 => m *m *cfn2_rec n' m + cfn2_rec n' m'
| 0, 0 => 1
| 0, _.+1 => 0
| _ .+1, 0 => 0
end.
Definition cfn2 := nosimpl cfn2_rec.
Notation "''U' ( n , m )" := (cfn2 n m)
(at level 8, format "''U' ( n , m )") : nat_scope.
Lemma foo n m:
n ^ (m.*2.+1) = \sum_(j<m.+1) (j.*2.+1)`! * 'U(m.+1,j.+1) * 'C(n+j, j.*2.+1).
Proof.
case m.
by rewrite n1bin big_ord_recr big_ord0 /= add0n muln1 mul1n addn0 //.
case.
rewrite n3bin 2! big_ord_recr big_ord0 /= addn1 add0n addn0 mul1n //.
case.
rewrite n5bin 3! big_ord_recr big_ord0 /= addn1 addn2 add0n addn0 mul1n //.
case.
rewrite 4! big_ord_recr big_ord0 /= addn1 addn2 addn3 add0n addn0 mul1n //.
transitivity ('C(n,1) + 126 * 'C(n.+1,3) +
1680 * 'C(n.+2,5) + 5040 * 'C(n.+3,7)).
admit.
done.
admit.
Qed.
Lemma exp3_addn a b: (a+b) ^3 = a^3 + a^2 *b *3 + a*b^2 * 3 + b^3.
Proof.
rewrite expnS sqrnD mulnDl 4!mulnDr.
have ->: a * (2 * (a * b)) = a^2 *b *2.
by rewrite -mulnA -mulnA (mulnA a b 2) (mulnC 2).
have ->: b * (2 * (a * b)) = a * b ^ 2 * 2.
by rewrite mulnC - mulnA (mulnC 2) mulnA.
rewrite -expnS -expnS (addnAC _ (b^3)) addnA; congr (_ + _).
rewrite - 3 !addnA; congr (_ + _).
rewrite addnC addnA -addnA (mulnC b); congr (_ + _).
by rewrite - (addn1 2) mulnDr muln1.
by rewrite - (addn1 2) mulnDr muln1.
Qed.
Lemma exp3_addn1 a: (a.+1) ^3 = a^3 + a^2 *3 + a * 3 + 1.
Proof. by rewrite -addn1 exp3_addn !muln1. Qed.
Lemma F14 n: (\sum_(i<n) ((i*2).+1)^3) = n^2 * (n ^2 * 2 - 1).
Proof.
elim: n; first by rewrite big_ord0.
move => n Hrec;rewrite big_ord_recr Hrec /= {Hrec}.
have aux:forall m, (m.+1 ^ 2 * 2 - 1) = m^2 *2 + m * 4 +1.
move => m; rewrite - addnA - (addn1 m) sqrnD mulnDl.
rewrite mulnDl addnAC muln1 mul1n mulnAC addn2 subn1 -pred_Sn.
by rewrite -addnS addn1 (mulnC _ m).
case: n => [// | n].
rewrite aux aux.
rewrite -addnA mulnDr -addnA.
rewrite -(addn2 n) sqrnD -addnA -addnA mulnDl (mulnDr (n^2)).
rewrite -addnA mulnCA; congr (_ + _).
set m := n.+1.
have ->: (2 ^ 2 + 2 * (n * 2)) = 4 * m.
by rewrite /m mulnC -(add1n n) mulnDr - mulnA mulnC.
rewrite (mulnDr (4 * m)).
have ->: 4 * m * (m ^ 2 * 2) = (m * 2)^3.
rewrite expnMn -mulnA (mulnA m) mulnC -mulnA //.
rewrite exp3_addn1 addnC [in X in _ = X] addnC -4! addnA; congr (_ + _).
have ->: (m * 2) ^ 2 * 3 = m^2 * 12 by rewrite expnMn -mulnA.
have ->: 4 * m * (m * 4 + 1) = m ^2 * 12 + ( m ^2 * 4 + m * 4).
rewrite addnA (mulnC 4) mulnDr muln1; congr (_ + _).
rewrite -(expnD (m * 4) 1 1) add1n expnMn (_: 4 ^2 = 12 + 4) //.
by rewrite mulnDr.
rewrite -addnA; congr (_ + _).
rewrite mulnDr mulnDr [in X in _ = X] addnC -addnA.
rewrite addnC (addnC 1) -addnA -addnA.
have r1: m^2 * 4 = n * m * 4 + m*4.
rewrite -mulnDl; congr (_ * _).
by rewrite expnS expn1 {1} /m -(addn1 n) mulnDl mul1n.
have ->: m ^ 2 * (n * 4) = n^2 * (m*4) + n * m *4.
rewrite mulnAC (mulnC n 4) mulnA r1 mulnC mulnDr ! mulnA.
by congr (_ + _); rewrite -(mulnA 4) mulnC.
rewrite -addnA; congr (_ + _).
rewrite muln1 muln1 (addnCA (n^2)) r1 -addnA; congr (_ + _).
rewrite addnA addnCA.
have ->: (m * 4 + m * 4 = m * 2 + m * 2 * 3) by rewrite - mulnA - !mulnDr.
rewrite addnA; congr (_ + _).
rewrite /m - (addn1 n) sqrnD -addnA -addnA; congr (_ + _).
rewrite !muln1 mulnDl mulnC addnCA; congr (_ + _).
Qed.
Lemma F22 n: \sum_(i<n) i `! * i = n `! .-1.
Proof.
elim: n; first by rewrite big_ord0.
move => n Hrec;rewrite big_ord_recr /= Hrec {Hrec}.
rewrite factS - {2 3} (prednK (fact_gt0 n)).
by rewrite -(add1n n) mulnDl mul1n addSn - pred_Sn mulnC.
Qed.
Lemma F23 n m: \sum_(i<m) 'C(n+i, n) = 'C(n+m, n.+1).
Proof.
elim: m; first by rewrite big_ord0 bin_small // addn0 //.
by move => m Hrec;rewrite big_ord_recr /= Hrec - binS addnS.
Qed.
Lemma F24_a n: n > 0 ->
\sum_(i<n) ( 'C(n, i.*2)) = \sum_(i<n) ('C(n, i.*2.+1)).
Proof.
case n; [by rewrite ltn0 | move => m _].
rewrite big_ord_recl bin0.
rewrite [X in 1 + X] (_:_ = \sum_(i < m) ('C(m, i.*2.+2) + 'C(m, i.*2.+1))) //.
transitivity (\sum_(i < m.+1) ('C(m, i.*2.+1) + 'C(m, i.*2))); last by [].
rewrite big_split big_split /= addnA addnC; congr ( _ + _).
rewrite big_ord_recr /= bin_small ?addn0 // ltnS -addnn; apply: leq_addr.
rewrite big_ord_recl bin0 //.
Qed.
Lemma F24_b (n: nat): n > 0 ->
\sum_(i<n.+1 | ~~ odd i) ( 'C(n, i)) = \sum_(i<n.+1 | odd i) ('C(n, i)).
Proof.
move => np.
rewrite [X in _ = X] (_: _ = \sum_(i < n.*2.-1 | ~~ odd i) 'C(n, i)).
rewrite big_mkcond [in X in _ = X ] big_mkcond /=.
move: np; case :n => [// | n _].
case: n => [|m]; first by rewrite 3! big_ord_recl 2! big_ord0 /=.
have -> : (m.+2).*2.-1 = m.+3 + ( (m.+2).*2.-1 - m.+3).
symmetry;apply: subnKC; rewrite 2! doubleS -pred_Sn 3! ltnS.
rewrite -addnn; apply : leq_addr.
rewrite big_split_ord /= [in X in _ = _ + X] big1 //.
move => i _; (case (odd (m + i)%Nrec)) => //=; rewrite bin_small //.
by rewrite 3!addSn 3! ltnS leq_addr.
transitivity (\sum_(i < n.*2 | odd i) 'C(n, i)).
rewrite big_mkcond [in X in _ = X] big_mkcond /=.
move: np; case :n => // m _.
have -> : (m.+1).*2 = m.+2 + ( (m.+1).*2 - m.+2).
symmetry;apply: subnKC; rewrite doubleS !ltnS -addnn; apply : leq_addr.
rewrite big_split_ord /= [in X in _ = _ + X] big1 //.
move => i _; (case (odd (m + i)%Nrec)) => //=; rewrite bin_small //.
rewrite addnC ! addnS ! ltnS; apply : leq_addl.
transitivity (\sum_(i<n) ('C(n, i.*2.+1))).
have pa: forall i: 'I_n, i.*2.+1 < n.*2.
by move => [i] hi /=; rewrite -doubleS leq_double.
have pb: forall i: 'I_(n.*2), i./2 < n.
move: np; case n; move => // m _ [i] hi /=.
move: hi; rewrite doubleS ltnS ltnS => lin.
by move: (half_leq lin) => /=; rewrite uphalf_double.
have pc: forall i: 'I_n.*2, odd i -> Ordinal (pa (Ordinal (pb i))) = i.
move => i oi; apply ord_inj => /=.
by rewrite -add1n - {2} (odd_double_half (nat_of_ord i)) oi.
rewrite (reindex_onto (fun i => Ordinal (pa i)) _ pc).
apply: congr_big => // i; apply /andP; split.
by case:i => i lin //=; rewrite odd_double.
apply /eqP; apply: ord_inj => /=; exact: uphalf_double.
transitivity (\sum_(i < n) 'C(n, i.*2)); first by rewrite F24_a.
have pa: forall i: 'I_n, i.*2 < n.*2.-1.
move: np; case n; move => // m _ [i] hi.
rewrite doubleS ltnS leq_double -ltnS //.
have pb: forall i: 'I_(n.*2.-1), i./2 < n.
move: np; case n; move => // m _ [i] hi /=.
move: hi; rewrite doubleS ltnS ltnS => lin.
by move: (half_leq lin) => /=; rewrite half_double.
have pc: forall i: 'I_n.*2.-1, ~~odd i -> Ordinal (pa (Ordinal(pb i))) = i.
move => i oi; apply ord_inj => /=.
by rewrite - {2} (odd_double_half (nat_of_ord i)) (negbTE oi).
symmetry;rewrite (reindex_onto (fun i => Ordinal (pa i)) _ pc).
apply: congr_big => // i;apply /andP; split.
by case:i => i lin //=; rewrite odd_double.
apply /eqP; apply: ord_inj => /=; exact: half_double.
Qed.
Lemma pascal11 n: \sum_(i < n.+1) 'C(n, i) = 2 ^ n.
Proof.
by rewrite (Pascal 1 1 n); apply: eq_bigr => i _ //; rewrite !exp1n !muln1.
Qed.
Lemma F24 n: n > 0 ->
\sum_(i<n.+1 | odd i) ( 'C(n, i)) = 2 ^ (n.-1).
Proof.
move => np.
have: \sum_(i < n.+1) 'C(n, i) = 2 ^ (n.-1) * 2.
by rewrite - expnSr (prednK np) pascal11.
rewrite (bigID (fun i : ordinal_finType n.+1 => odd i)) /= (F24_b np).
by move /eqP; rewrite addnn - muln2 (eqn_pmul2r (ltn0Sn 1)); move /eqP.
Qed.
Lemma F25 n: n > 0 ->
\sum_(i<n.+1 | ~~ odd i) 'C(n, i) = 2 ^ (n.-1).
Proof. by move => np; rewrite (F24_b np) F24. Qed.
Lemma G5_a r t q:
\sum_(i<r.+1) ( 'C(t+r - i, t) * 'C(q + i, q) ) = 'C(q+t+r+1,r).
Proof.
move: t; elim:r.
by move => t ; rewrite bin0 big_ord_recl /= big_ord0 ! addn0 subn0 !binn.
move => n H; elim => [| t H1].
rewrite addn0 addnAC addn1 - binom_mn_n - {1} (addn1 q) - addnA add1n - F23.
by apply: eq_bigr => i _;rewrite bin0 mul1n.
transitivity ( \sum_(i < n.+1) 'C(t.+1 + n - i, t.+1) * 'C(q + i, q)
+ \sum_(i < n.+2) 'C(t + n.+1 - i, t) * 'C(q + i, q)).
rewrite big_ord_recr (big_ord_recr (n.+1)) /= !addnK !binn !mul1n addnA.
congr (_ + _); rewrite - big_split; apply: eq_bigr => i _ /=.
rewrite - mulnDl; congr (_ * _); case : i => [j] /=; rewrite ltnS => je.
by rewrite - 2! addSnnS - (addnBA _ je) - binS - (addnBA _ je) - addSn.
by rewrite H H1 !addn1 -(addnA q t) -(addSnnS t n) (addnA q) addnC (addnS _ n).
Qed.
Lemma G5_b n p q: p <= n -> q <p ->
\sum_(q+1 <= k < (n - p + q + 1).+1) ( 'C(n-k, p-q-1) * 'C(k-1, q)) = 'C(n,p).
Proof.
move => pa pb.
rewrite - (bin_sub pa) - addnA - subnDA addn1.
move: (subnK pb); set r := n - p; set t := p - q.+1 => pc.
have pd : n = q+t+r+1.
by rewrite (addnC _ r) - addnA - (subnK pa) (addnC q) -addnA addn1 pc.
rewrite - {1} (add0n (q.+1)) big_addn big_mkord.
rewrite (subSn (leq_addl r q.+1)) addnK pd -G5_a.
apply:congr_big => // i _; congr (_ * _); last by rewrite addnS subn1 addnC.
case i => [m] /=; rewrite ltnS => mr; congr ('C(_, t)).
rewrite - (addnBA t mr) (addnC q) -addnA -addnA (addnCA q) addn1.
by rewrite - {1} (subnK mr) - addnA addnA addnK.
Qed.
Compute the sum of binomial coefficients with alternate signs
Definition Ftype m n := {ffun 'I_m -> 'I_n.+1}.
Definition monomial_lt m n (f:Ftype m n) := \sum_(i<m) (f i) < n.
Definition monomial_le m n (f:Ftype m n) := \sum_(i<m) (f i) <= n.
Definition monomial_eq m n (f:Ftype m n) := \sum_(i<m) (f i) == n.
Lemma card_set_pred: forall (T:finType) (P:T -> bool),
#|[set f:T | P f]| = #|[pred f:T | P f]|.
Proof. by move => T P; apply: eq_card; move => t; rewrite in_set //. Qed.
Lemma G3_a (m n: nat): #|[set f:Ftype m n | monomial_le f ]|
= #|[set f:Ftype m n | monomial_eq f ]|
+ #|[set f:Ftype m n | monomial_lt f ]|.
Proof.
symmetry; rewrite ! card_set_pred.
rewrite - (cardID [pred f | monomial_eq f] [pred f | monomial_le f]).
congr (_ + _).
apply: eq_card => f; rewrite !inE /monomial_eq /monomial_le.
by case: eqP; [ move => -> //=; rewrite leqnn | rewrite andbF].
by apply: eq_card => f; rewrite !inE /monomial_lt ltn_neqAle.
Qed.
Lemma G3_b (m n: nat):
#|[set f:Ftype m n.+1 | monomial_lt f ]| =
#|[set f:Ftype m n | monomial_le f ]|.
Proof.
pose R (f:Ftype m n) := [ffun i:'I_m => widen_ord (leqnSn n.+1) (f i)].
have injR: (injective R).
move => f g ; rewrite - ffunP - ffunP => sr i; apply: ord_inj.
move: (sr i); rewrite /R !ffunE => eq1.
by move: (f_equal (@nat_of_ord n.+2) eq1).
symmetry; rewrite card_set_pred - (card_image injR [pred f | monomial_le f]).
rewrite - imset_card.
apply: eq_card=> s; rewrite in_set; apply /imsetP; case:ifP.
rewrite /monomial_lt => les.
have vln: forall i, s i < n.+1.
move => i; move: les; rewrite (bigD1 i) //=.
apply: leq_trans;apply: leq_addr.
pose x:= [ffun i:'I_m => Ordinal (vln i)].
exists x.
rewrite inE /=; move: les; rewrite /monomial_le ltnS.
have -> //: \sum_(i < m) s i = \sum_(i < m) x i.
by apply: eq_big => // i _; rewrite /x ffunE.
by rewrite /R -ffunP => i; rewrite ffunE ffunE; apply: ord_inj.
move=> lef [x]; rewrite inE /=; move => lex sr; move: lef lex.
rewrite /monomial_lt /monomial_le sr /R /= ltnS.
set s1 := \sum_(i < m) _; set s2 := \sum_(i < m) _.
have : s1 = s2 => [ | -> -> // ].
by apply: congr_big => // i _; rewrite ffunE.
Qed.
Lemma G3_c (n: nat): #|[set f:Ftype 0 n | monomial_le f ]| = 1.
Proof.
set f0: (Ftype 0 n):= [ffun _ => ord0].
apply /eqP/cards1P; exists f0; rewrite -setP => g; rewrite in_set1 in_set.
by apply/eqP; case:ifP; [ rewrite big_ord0 | case/eqP /ffunP; case].
Qed.
Lemma G3_d (m: nat): #|[set f:Ftype m 0 | monomial_le f ]| = 1.
Proof.
set f0: (Ftype m 0):= [ffun _ => ord0].
apply /eqP/cards1P; exists f0; rewrite -setP => g; rewrite in_set1 in_set.
apply/eqP; case:ifP.
by move /eqP => ->; rewrite subn0 big1 => // => i _; rewrite /f0 ffunE.
move /eqP; case; rewrite - ffunP; move => t; rewrite /f0 ffunE.
by apply: val_inj; case: (g t); case.
Qed.
Lemma G3_e (m n: nat): #|[set f:Ftype m.+1 n | monomial_eq f ]|
= #|[set f:Ftype m n | monomial_le f ]|.
Proof.
set T:= Ftype m.+1 n.
pose restr (f:T):= [ffun z:'I_m => f (widen_ord (leqnSn m) z)].
have restr_pr1: forall f: T, monomial_eq f ->
n = \sum_(i<m) ((restr f) i) + f ord_max.
move => f; rewrite /monomial_eq; move /eqP => le1.
rewrite -{1}le1 big_ord_recr /restr; congr( _ + _) =>//=.
by apply: congr_big => // i _ /=; rewrite ffunE.
have restr_pr2: forall f: T, monomial_eq f -> monomial_le (restr f).
move => f feq; rewrite /monomial_le {3} (restr_pr1 _ feq); apply: leq_addr.
have restr_inj: {in [pred f | (monomial_eq f)] &, injective restr}.
move => f1 f2.
rewrite !inE => meq1 meq2 sr;rewrite - ffunP => i.
move: (ltn_ord i); rewrite ltnS leq_eqVlt; case /orP => lim.
have -> : i = ord_max by apply: ord_inj;by move:lim; move /eqP => ->.
apply: ord_inj.
by apply: (@addnI (\sum_(i < m) (restr f1) i)); rewrite {2} sr - !restr_pr1.
move: sr;rewrite - ffunP => sr; move: (sr (Ordinal lim)).
rewrite !ffunE.
have -> // : (widen_ord (leqnSn m) (Ordinal lim)) = i; by exact: ord_inj.
move: (card_in_imset restr_inj); rewrite - card_set_pred.
rewrite - [in X in (_ = X)]card_set_pred; move => <-.
apply:eq_card => f; rewrite in_set in_set; apply /imsetP.
case: ifP => lef; last first.
by move=> [x]; rewrite inE => meq fr; move:lef; rewrite fr restr_pr2.
move: (leq_subr (\sum_(i < m) f i) n); rewrite -ltnS => le2.
pose g := [ffun i:'I_(m.+1) => if (unlift ord_max i) is Some j then f j
else (Ordinal le2)].
have gi : forall i: 'I_m, g (widen_ord (leqnSn m) i) = f i.
move => i; rewrite /g ffunE.
have -> : (widen_ord (leqnSn m) i) = (lift ord_max i).
by apply: ord_inj; rewrite lift_max.
by rewrite liftK.
have gs: \sum_(i < m) g (widen_ord (leqnSn m) i) = \sum_(i < m) f i.
by apply: congr_big => // i _; move: (gi i) => /= ->.
exists g.
rewrite !inE /monomial_eq big_ord_recr gs /g ffunE unlift_none /=.
by rewrite addnC subnK.
by rewrite - ffunP => i; rewrite ffunE gi.
Qed.
Lemma G3_f m n: #|[set f:Ftype m n | monomial_le f ]| = 'C(n+m,m).
Proof.
move:n;elim: m; first by move => n; rewrite bin0 G3_c.
move => n hrec.
elim; first by rewrite add0n binn G3_d.
by move => m hrec1;rewrite G3_a G3_b G3_e addnC hrec1 hrec !addnS binS.
Qed.
Lemma subseq_iota a n b m : b <=a -> a + n <= b + m ->
subseq (iota a n) (iota b m).
Proof.
move => ba.
move: (subnK ba); rewrite addnC => <-; rewrite - addnA leq_add2l => le1.
move: (leq_trans (leq_addr n (a-b)) le1) => aux.
move: (iota_add b (a-b)(m -(a-b))); rewrite addnC (subnK aux) => ->.
rewrite -{1}(cat0s (iota (b + (a - b)) n)); apply: cat_subseq => //.
apply: sub0seq.
have nm: n <= (m - (a - b)) by rewrite -(leq_add2l (a-b)) subnKC //.
set c := (b + (a - b)); move: (iota_add c n ((m - (a - b)) - n)).
rewrite addnC (subnK nm) => ->.
rewrite -{1}(cats0 (iota c n)); apply: cat_subseq => //; apply: sub0seq.
Qed.
Lemma subseq_iota1 i m: i<m -> subseq ([:: i; i.+1]) (iota 0 m.+1).
Proof.
have ->: [:: i; i.+1] = iota i 2 by [].
by move => im; apply: subseq_iota => //; rewrite add0n addn2 ltnS.
Qed.
Lemma sorted_prop f m:
sorted ltn (mkseq f m.+1) <-> (forall i, i<m -> f i < f (i.+1)).
Proof.
split.
move => h i im.
move: (map_subseq f (subseq_iota1 im)); rewrite -/(mkseq f m.+1) => pb.
have tr_ltn: (transitive ltn) by move => a b c ; apply: ltn_trans.
by move: (subseq_sorted tr_ltn pb h)=> /=; rewrite andbT.
move => fi. simpl.
move: m f fi; elim => [ //= | n hrec f fi /=].
rewrite (fi 0 (ltn0Sn n)) /=.
set f' := f \o (addn 1).
have fi': (forall i, i < n -> f' i < f' i.+1) by move => i lin; rewrite fi.
move: (hrec _ fi'); rewrite map_comp /f' /= addn0 - iota_addl //.
Qed.
Lemma G3_f' (m n: nat):
#|[set f:Ftype m n | monomial_le f ]| = 'C(n+m,m).
Proof.
case:m; first by rewrite bin0 G3_c.
move => m.
rewrite addnS - card_ltn_sorted_tuples.
set Ta:= Ftype m.+1 n.
pose toseq (f:Ta) := map_tuple [ffun z:'I_(m.+1) =>
@inord (n+m) (\sum_(i<(m.+1) | i<=z) (f i) + z)]
(ord_tuple (m.+1)).
pose ps (f:Ta) z := \sum_(i<(m.+1) | i<=z) (f i) + z.
have ps0: forall (f: Ta), ps f 0 = f ord0.
move => f; rewrite /ps addn0 (big_pred1 ord0) //= => t /=.
by rewrite /leq subn0.
have psr: forall (f: Ta), forall z (H: z.+1 < m.+1),
ps f z.+1 = (ps f z) + (f (Ordinal H)) +1.
move => f z h; rewrite /ps.
rewrite addnS - addn1; congr (_ + 1); rewrite addnAC; congr (_ + z).
rewrite addnC (bigD1 (Ordinal h)) //=; congr (_ + _).
by apply: eq_bigl => s; rewrite -(ltnS s z) ltn_neqAle andbC.
have psi: forall f g, (forall i, i< m.+1 -> ps f i = ps g i) -> f = g.
move => f g fgi; rewrite - ffunP; case => i => ile; move: ile; case:i.
move => h //.
have ->: Ordinal h = ord0 by apply: ord_inj.
by apply: ord_inj; rewrite - (ps0 f) - (ps0 g) fgi.
move => i ile; apply: ord_inj.
move: (fgi _ ile); rewrite psr psr - (fgi _ (leq_trans (leqnSn i) ile)).
by move /eqP; rewrite eqn_add2r eqn_add2l; move /eqP.
have toseq1: forall f:Ta, monomial_le f ->
forall z: 'I_(m.+1), ps f z <= n + m.
move =>f mle z; apply: leq_add; last by move: z => [z] i //=.
apply: leq_trans mle.
rewrite (bigID (fun i:'I_(m.+1) => i <= z) xpredT) /= ; apply: leq_addr.
have toseq2: forall f:Ta, monomial_le f -> forall z: 'I_(m.+1),
nat_of_ord (@inord (n+m) (ps f z)) = ps f z.
by move => f mle z; move: (toseq1 f mle z) => le2 /=; rewrite insubdK.
have toseq3: forall f:Ta, monomial_le f -> forall z: 'I_(m.+1),
nat_of_ord (tnth (toseq f) z) = ps f z.
by move => f mle z; rewrite tnth_map tnth_ord_tuple ffunE toseq2.
have toseq_inj: {in [pred f | (monomial_le f)] &, injective toseq}.
move => f1 f2; rewrite !inE /= => fle1 fle2 sseq; apply: psi => i lim.
move: (toseq3 _ fle1 (Ordinal lim)) => /= <-.
by rewrite sseq (toseq3 _ fle2 (Ordinal lim)).
have toseq4: forall f:Ta, monomial_le f ->
(map val (toseq f)) = mkseq (ps f) m.+1.
move => f mle.
have s1: size (map val (toseq f)) = m.+1.
by rewrite size_map size_map size_tuple.
apply: (eq_from_nth (x0:=0)).
by rewrite s1 size_mkseq.
move => i; rewrite s1 => lim.
set k := (tnth_default (toseq f) (Ordinal lim)).
have lim1: i < size (toseq f) by rewrite size_map size_tuple.
rewrite (nth_mkseq _ _ lim) (nth_map k 0) //.
have ->: (nth k (toseq f) i) = tnth (toseq f) (Ordinal lim) by [].
by move: (toseq3 f mle (Ordinal lim)) => /= <-.
have toseq_ord: forall f:Ta,
monomial_le f -> sorted ltn (map val (toseq f)).
move => f mle.
rewrite (toseq4 _ mle) sorted_prop => i im.
by rewrite psr; rewrite addn1 ltnS leq_addr.
rewrite card_set_pred - (card_in_image toseq_inj).
rewrite - card_set_pred; apply: eq_card => g.
rewrite ! in_set; apply/mapP.
case: ifP; last first.
move=> lef [x]; rewrite mem_enum inE /= => meq fr.
by move:lef; rewrite fr; move /negP; apply; apply: toseq_ord.
pose v1 i := val (tnth g (inord i)).
have v1p: forall i:'I_m.+1, v1 i = val (tnth g i).
move => i; rewrite /v1 inord_val ; congr (tnth g _) => /=; apply: val_inj.
have ->: (map val g) = mkseq v1 m.+1.
rewrite - map_tnth_enum -map_comp /mkseq - val_enum_ord -(map_comp v1).
by apply /eq_in_map => i _ => /=; rewrite v1p.
rewrite sorted_prop => vi.
pose v2 i := v1 (i.+1) - v1 (i) -1.
have v2p: forall i, i<m -> v1 i.+1 = v1 i + v2 i +1.
move => i im; move: (vi _ im); rewrite /v2 => cp1.
by rewrite addnAC - subnDA addn1 - {1}(subnKC cp1).
pose v2' i := if i is j.+1 then v2 j else v1 0.
pose v3 z := (\sum_(i<(m.+1) | i<=z) (v2' i) + z).
have v30: v3 0 = v1 0.
rewrite /v3 addn0 (big_pred1 ord0) //= => t /=.
by rewrite /leq subn0.
have v3r: forall z, z < m -> v3 z.+1 = v3 z + (v2 z) +1.
move => z h; rewrite /v3; rewrite - ltnS in h.
rewrite addnS - addn1; congr (_ + 1); rewrite addnAC; congr (_ + z).
rewrite addnC (bigD1 (Ordinal h)) //=; congr (_ + _).
by apply: eq_bigl => s; rewrite -(ltnS s z) ltn_neqAle andbC.
have v31: forall z, z < m.+1 -> v3 z = v1 z.
elim => [ // | i hrec]; rewrite ltnS => im.
by rewrite (v3r _ im) (v2p _ im) hrec //; apply:(ltn_trans im (ltnSn m)).
have v3m: v3 m = (\sum_(i<(m.+1)) (v2' i) + m).
by rewrite /v3; congr ( _ + m); apply: congr_big => //; case.
have v1in: forall i, i<m.+1 -> v1 i < (n + m).+1.
by move => i lim; rewrite /v1; set x := tnth _ _; case x => [j] imn.
have svln: \sum_(i < m.+1) (v2' i) <= n.
by rewrite - (leq_add2r m) - v3m (v31 m (ltnSn m)) -ltnS (v1in m (ltnSn m)).
have vln: forall i, i < m.+1 -> v2' i < n.+1.
move => i lim; rewrite ltnS; move: svln.
rewrite (bigD1 (Ordinal lim)) //=; apply: leq_trans;apply: leq_addr.
set f:= [ffun i:'I_(m.+1) => (Ordinal (vln _ (ltn_ord i)))].
have sf: \sum_(i < m.+1) f i = \sum_(i < m.+1) v2' i.
by apply: congr_big => //; move => [i] im _; rewrite ffunE.
exists f; first by rewrite mem_enum inE /= /monomial_le sf.
apply: eq_from_tnth => i.
apply: val_inj; rewrite -v1p tnth_map tnth_ord_tuple ffunE.
have -> : \sum_(i0 < m.+1 | i0 <= i) f i0 + i = v3 i.
by rewrite /v3; congr(_ + i); apply: congr_big => // j ji; rewrite ffunE//.
symmetry; rewrite v31 => //; rewrite inord_val //.
Qed.
Lemma F6_aux n: n ^2 = 2 * 'C(n,2) + 'C(n,1).
Proof.
case: n => // n; rewrite bin2 bin1 succnK mul2n - mulnn mulnSr.
by move:(odd_double_half (n.+1 * n)); rewrite odd_mul /= andNb add0n => ->.
Qed.
Lemma F7_aux n: n ^ 3 = 6 * 'C(n, 3) + 6 * 'C(n, 2) + 'C(n, 1).
Proof.
elim:n => //n Hrec; rewrite - {1} addn1 Pascal 4! big_ord_recr big_ord0 /=.
rewrite !exp1n expn0 expn1 !muln1 add0n /subn /= bin0 bin1 mul1n Hrec.
rewrite (_: 'C(3, 2) = 3) // !binS !mulnDr bin0 addnA; congr (_ + 1).
rewrite - 5!addnA (addnC ('C(n, 1))); congr (_ + (_ + (_ + _))).
by rewrite F6_aux mulnDr mulnA bin1 - addnA addnn - mul2n mulnA.
Qed.
Lemma F8_aux n:
n ^ 4 = 24 * 'C(n, 4) + 36 * 'C(n, 3) + 14 * 'C(n, 2) + 'C(n, 1).
Proof.
elim:n => //n Hrec; rewrite - {1} addn1 Pascal 5! big_ord_recr big_ord0 /=.
rewrite !exp1n expn0 expn1 !muln1 add0n /subn /= bin0 bin1 mul1n Hrec.
rewrite !(binS n) 3! mulnDr bin0 addnA;congr (_ + 1).
set a := 24 * 'C(n, 4); set b := 36 * 'C(n, 3).
rewrite - 5! addnA -(addnA (a + _)) (addnAC a) - (addnA b).
rewrite (addnCA ( 36 * 'C(n, 2))) - 4! addnA; congr (_ + (_ + (_ + _))).
rewrite (_: 'C(4, 2) = 6) // (_: 'C(4, 3) = 4) // F7_aux bin1.
rewrite (addnC _ (_ + n)) (addnC (24 * _)) - (addnA n); congr (n + _).
rewrite - addnA mulnDr mulnA - addnA; congr (_ + _).
rewrite F6_aux 2! mulnDr 2! mulnA bin1 - (addnA _ _ (4 * n)) - mulnDl.
by rewrite addnAC addnA - mulnDl - addnA - mulnDl.
Qed.
Lemma F9_aux n:
n ^ 5 = 120 * 'C(n, 5) + 240 * 'C(n, 4) + 150 * 'C(n, 3) +
30 * 'C(n, 2) + 'C(n, 1).
Proof.
elim:n => //n Hrec; rewrite - {1} addn1 Pascal 6! big_ord_recr big_ord0 /=.
rewrite !exp1n expn0 expn1 !muln1 add0n /subn /= bin0 bin1 mul1n Hrec {Hrec}.
set a:= 120; set b := 240; set c := 150; set d := 30.
symmetry;rewrite 5!binS bin0;rewrite addnA; congr (_ + 1).
rewrite -10 ! addnA !mulnDr -addnA;congr (_ + _).
rewrite addnC -2!addnA; congr (_ + _); rewrite addnC -3!addnA; congr (_ + _).
rewrite addnC -3!addnA; congr (_ + _);rewrite addnC -3!addnA; congr (_ + _).
rewrite F8_aux 3! mulnDr 3!mulnA -3!addnA; congr (_ + _).
rewrite (addnCA (5 * 'C(n, 1))) (addnCA (5 * 14 * 'C(n, 2)))(_: 'C(5,2) = 10) //.
rewrite F7_aux 2!mulnDr 2!mulnA - 2!addnA (addnA (5 * 36 * 'C(n, 3))).
rewrite - mulnDl {1} (_: c = 10 * 6 + 90) // mulnDl - addnA.
congr (_ + (_ + _)); rewrite F6_aux bin1.
rewrite (addnC (10 * n)) (_: 'C(5,3) = 10) // (_: 'C(5,4) = 5) //.
rewrite mulnDr mulnA - (addnA _ _ (5 * n)) - mulnDl (addnC (5 * n)).
by rewrite -(addnA _ _ (5 * n)) -mulnDl addnA -mulnDl -addnA -mulnDl.
Qed.
Lemma F36 k l i:
(\sum_(j < i.+1) ('C(k, j) *'C(l, (i - j)))) = 'C(k+l , i).
Proof.
pose f k i := (\sum_(j < i.+1) 'C(k, j) * 'C(l, i - j)).
rewrite -/(f k i) ; move: k i.
have fx0: forall k, f k 0 = 'C(k + l, 0).
by move=> k; rewrite /f big_ord_recl big_ord0 addn0 !bin0 muln1.
have f0x: forall i, f 0 i = 'C(l, i).
move=> i; rewrite /f big_ord_recl bin0 mul1n big1 ? addn0 ?subn0 //.
suff fxx: forall k i, f (k.+1) (i.+1) = f k i.+1 + f k i.
by elim => [//| k h1]; elim => [//| i h2]; rewrite fxx h1 h1 - binS addSn.
move=> k i; rewrite /f big_ord_recl (big_ord_recl (i.+1)) !bin0 !mul1n -addnA.
congr (_ + _); rewrite -big_split /=.
by apply: eq_bigr => j _ ; rewrite - mulnDl.
Qed.
Lemma F37 n p: p<= n ->
(\sum_(k < (n-p).+1) ('C(n, k) *'C(n, p+k))) = 'C(2*n,n-p).
Proof.
move => h; move: (subnK h); set q := n - p; move => <-.
move: (F36 (q+p)(q +p) q);rewrite addnn - mul2n => <-.
apply: eq_bigr; move => [j] /=; rewrite ltnS => jq _.
by rewrite addnC - (@bin_sub (p + q) (p + j)) ?leq_add2l // subnDl.
Qed.
Lemma F38 n: \sum_(i<n.+1) 'C(n,i) ^2 = 'C(n.*2, n).
Proof.
rewrite - addnn - (F36 n n n); apply: congr_big => // [[i isn]].
by rewrite expnS expn1 bin_sub //.
Qed.
Lemma F27_a n: \sum_(i < n.+1) i* 'C(n, i) = n * 2 ^ (n.-1) .
Proof.
elim:n; first by rewrite big_ord_recr big_ord0 mul0n //.
move => n Hrec; rewrite big_ord_recl mul0n add0n /= big_split /=.
have ->: \sum_(i < n.+1) 'C(n.+1, bump 0 i) =
\sum_(i < n.+1) 'C(n, bump 0 i) + \sum_(i < n.+1) 'C(n,i).
rewrite - big_split /=; apply: eq_bigr; move => [i lin] _ //=.
rewrite addnAC pascal11 mulSnr; congr (_ + _).
have ->: n * 2 ^ n = n * 2 ^ n.-1 + n * 2 ^ n.-1.
by case n => // m /=; rewrite addnn - muln2 expnSr mulnA.
rewrite [X in _ + X] (_ :_ = \sum_(i < n.+1) i*'C(n, bump 0 i) + n * 2 ^ n.-1).
rewrite addnA - {2} Hrec; congr (_ + _);rewrite - big_split /=.
rewrite [X in _ = X] big_ord_recl big_ord_recr bin_small //=.
rewrite mul0n muln0 !addn0 add0n; apply: eq_bigr => i _ /=; rewrite -mulSn //.
by rewrite - Hrec - big_split /=; apply: eq_bigr => i _; rewrite - mulnDr.
Qed.