proposition: Lemma included_trans : transitive included.
proof: Proof. move=> shb sha shc. move=> /includedP[Hsza Hincla] /includedP[Hszb Hinclb]. apply/includedP; split; first exact (leq_trans Hsza Hszb). by move=> i; exact: leq_trans (Hincla i) (Hinclb i). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype