proposition: Lemma prs_is_equivalence y x: partition_s y x -> equivalence (partition_relset y x).
proof: Proof. move=> pa; apply: isc_rel_equivalence; first by apply: pfs_f. by apply: pfs_partition. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)