proposition: Lemma G3_e (m n: nat): #|[set f:Ftype m.+1 n | monomial_eq f ]| = #|[set f:Ftype m n | monomial_le f ]|.
proof: 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; move: (restr_pr1 _ feq). move: (\sum_(i < m) restr f i) => n0 Hn. by rewrite Hn; 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_m.+1 -> 'I_n.+1} := [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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)