proposition: Lemma image_pre (B : pred T') : image f [preim f of B] =i [predI B & codom f].
proof: Proof. by move=> y; rewrite /image_mem -filter_map /= mem_filter -enumT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)