proposition: Lemma preim_partitionP D : partition (preim_partition D) D.
proof: Proof. by apply/equivalence_partitionP; split=> // /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)