proposition: Lemma preim_omap_None (aT rT : finType) (f : aT -> rT) : (omap f @^-1 None) = [set None].
proof: Proof. apply/setP => x. rewrite -mem_preim !inE. by case: x => [x|]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)