proposition: Lemma is_finer_trans : transitive is_finer.
proof: Proof. move=> P1 P2 P3 /is_finer_pblockP P12 /is_finer_pblockP P23. apply/is_finer_pblockP=> x xinS. exact: (subset_trans (P12 _ xinS) (P23 _ xinS)). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition