proposition: Lemma preim_omap_Some (aT rT : finType) (f : aT -> rT) y : (omap f @^-1 Some y) = Some @: (f @^-1 y).
proof: Proof. apply/setP => [[x|]] //=; rewrite !inE /= ?Some_eqE. - apply/idP/imsetP => E. exists x => //. by rewrite -mem_preim. case: E => x0 ? [->]. by rewrite mem_preim. - by apply/idP/imsetP => // [[?]] //. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)