proposition: Lemma join_finer_eq_in_S P Q x y : x \in S -> join_finer_eq P Q x y -> y \in S.
proof: Proof. move=> xinS /connectP => [[pth Hpth Hlast]]. elim: pth x Hpth Hlast xinS => [x /= _ -> // | x p0 IH xn /=]. case/andP=> [H1 {}/IH/[apply]/[swap] xninS]; apply. by move: H1=> /orP[]; apply: mem_pblock_setpart. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition