proposition: Lemma codomfPn f v : reflect (forall x, f.[? x] != Some v) (v \notin codomf f).
proof: Proof. rewrite mem_codomf negb_exists; apply: (iffP forallP) => f_eq_v x /=. by case: fndP => //= kf; rewrite f_eq_v. by apply: contraNneq (f_eq_v (val x)) => <-; rewrite Some_fnd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)