proposition: Lemma imset_partition : partition P D = partition fP (f @: D).
proof: Proof. suff cov: (cover fP == f @:D) = (cover P == D). by rewrite /partition -imset_trivIset imset0mem cov. by rewrite /fP cover_imset -imset_cover (inj_eq imset_inj). Qed.
imports: mathcomp(all_ssreflect)