proposition: Fact join_intpartnP sh1 sh2 sh : (join_intpartn sh1 sh2 <= sh)%O = (sh1 <= sh)%O && (sh2 <= sh)%O.
proof: Proof. rewrite /join_intpartn /= -{1}(conj_intpartnK sh). by rewrite partdom_conj_intpartn meet_intpartnP !partdom_conj_intpartn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype