proposition: Lemma mcoeff_lt_mlast p m : (m < mlast p)%O -> p@_m = 0.
proof: Proof. move=> le; case/boolP: (m \in msupp p). by move/mlast_lemc/(lt_le_trans le); rewrite ltxx. by rewrite mcoeff_msupp negbK => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg