proposition: Lemma can2_mem_pmap : pcancel g f -> forall s u, (u \in pmap f s) = (g u \in s).
proof: Proof. by move=> gK s u; rewrite -(mem_map (pcan_inj gK)) pmap_filter // mem_filter gK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)