proposition: Lemma mlead_deg p : p != 0 -> (mdeg (mlead p)).+1 = msize p.
proof: Proof. move=> /mlead_supp lc_in_p; rewrite /mlead msizeE mdeg_bigmax. have: msupp p != [::] by case: (msupp p) lc_in_p. elim: (msupp p)=> [|m [|m' r] ih] // _; first by rewrite !big_seq1. by rewrite big_cons -maxnSS {}ih // !big_cons. 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