proposition: Lemma G3_f' (m n: nat): #|[set f:Ftype m n | monomial_le f ]| = 'C(n+m,m).
proof: 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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)