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