proposition: Lemma equivalence_partitionE (T : finType) (R S : rel T) (D : {set T}) : R =2 S -> equivalence_partition R D = equivalence_partition S D.
proof: Proof. rewrite /equivalence_partition=> eq_RS. by apply eq_imset=> x; apply/setP=> y; rewrite !inE eq_RS. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition