proposition: Lemma card_preim (B : {pred T'}) : #|[preim f of B]| = #|[predI codom f & B]|.
proof: Proof. rewrite -card_image /=; apply: eq_card => y. by rewrite [y \in _]image_pre !inE andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)