proposition: Lemma le_intpartndomlexi d : {homo (id : 'PDom_d -> 'PLexi_d) : x y / (x <= y)%O}.
proof: Proof. move=> sh1 sh2. rewrite leEpartdom leEintpartnlexi leEseqlexi. case: sh1 => [sh1 /andP[/eqP Hsum1 Hpart1]] /=. case: sh2 => [sh2 /andP[/eqP Hsum2 Hpart2]] /=. move: Hsum1; rewrite -{}Hsum2. elim: sh1 Hpart1 sh2 Hpart2 => [|s01 sh1 IHsh] Hpart1 sh2 Hpart2. by move/esym/(part0 Hpart2) => ->. case: sh2 Hpart2 => [|s02 sh2] Hpart2 //=. move: Hpart1 => /part_head_non0 /= /negbTE H0 /eqP. by rewrite addn_eq0 H0. move: Hpart1 => /= /andP[_ Hpart1]. move: Hpart2 => /= /andP[_ Hpart2]. move=> Hsum Hdom. have /partdomP/(_ 1) := Hdom; rewrite /= !take0 /= !addn0 => les0. rewrite !leEnat les0 /= leqNgt. move: les0; rewrite leq_eqVlt => /orP[/eqP Heq|->]//. subst s02; rewrite ltnn /= leEseqlexi; apply: IHsh => //. by move: Hsum => /eqP; rewrite eqn_add2l => /eqP. exact: (partdom_consK Hdom). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype