fact: Fixpoint included inner outer := if inner is inn0 :: inn then if outer is out0 :: out then (inn0 <= out0) && (included inn out) else false else true.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype