proposition: Lemma is_finer_refl : reflexive is_finer.
proof: Proof. by move=> P; apply/is_finer_pblockP=> x _. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition