proposition: Fact meet_intpartnP sh sh1 sh2 : (sh <= meet_intpartn sh1 sh2)%O = (sh <= sh1)%O && (sh <= sh2)%O.
proof: Proof. apply/idP/andP => [Hmeet | [/partdomP H1 /partdomP H2]]. split; apply: (le_trans Hmeet); first exact: le_meet_intpartn. by rewrite meet_intpartnC le_meet_intpartn. apply/partdomP => i. case: (ltnP i d.+1) => [Hi | /ltnW Hi]; first last. by rewrite !take_intpartn_over // !sumn_intpartn. rewrite sumn_take_part_fromtuple // nth_parttuple_minn //. by rewrite leq_min H1 H2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype