proposition: Lemma mleadDr (p1 p2 : {mpoly R[n]}) : (mlead p1 < mlead p2)%O -> mlead (p1 + p2) = mlead p2.
proof: Proof. move=> lt_p1p2. apply/le_anti. move/ltW/join_r: (lt_p1p2) (mleadD_le p1 p2) => -> -> /=. rewrite leNgt; apply/negP=> /mcoeff_gt_mlead. rewrite mcoeffD mcoeff_gt_mlead // add0r => /eqP. rewrite mleadc_eq0=> /eqP z_p2; move: lt_p1p2. by rewrite z_p2 mlead0 ltx0. 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