proposition: Lemma join_finerC : commutative join_finer.
proof: Proof. rewrite /join_finer=> P Q; apply val_inj=> /=. apply equivalence_partitionE => x y; apply eq_connect => {}x {}y /=. exact: orbC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition