proposition: 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: 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.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)