proposition: Lemma In_findN k f : reflect (find k f = None) (k \notin dom f).
proof: Proof. case: In_domX=>H; constructor. - by case: H=>x /In_find ->. by apply/find_none/negP=>/In_domX [v X]; apply: H; exists v. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)