proposition: Lemma In_rangeX v f : v \In range f <-> exists k, (k, v) \In f.
proof: Proof. elim/um_indf: f v=>[v|v|k w f IH W P v]. - by rewrite range_undef; split=>//; case=>x /In_undef. - by rewrite range0; split=>//; case=>x /In0. move: (order_path_min (@trans K) P)=>A. rewrite /range assocsPtUn //= InE; split. - case=>[->|/IH [k' H]]; first by exists k; rewrite InPtUnE //; left. by exists k'; rewrite InPtUnE //; right. case=>k'; rewrite InPtUnE //; case; first by case; left. by move=>H; right; apply/IH; exists k'. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)