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