proposition: Lemma join_finer_equivalence P Q : {in S & &, equivalence_rel (join_finer_eq P Q)}.
proof: Proof. split; first exact: connect0. rewrite /join_finer_eq=> cxy. rewrite -(same_connect _ cxy) // {cxy H H0 H1 x y z}. by apply: relU_sym; apply: setpart_conn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition