proposition: Fact emptypart_bottom sh : (empty_intpart <= sh :> 'YL)%O.
proof: Proof. by apply/includedP; split => //= i; rewrite nth_nil. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype