proposition: Lemma index_dom_range_mem f k t : index k (dom f) = index t (range f) -> index k (dom f) != size (dom f) -> (k, t) \In f.
proof: Proof. rewrite /range assocs_dom. elim/um_indf: f k t=>[||k' t' f IH W /(order_path_min (@trans K)) P] k t. - by rewrite assocs_undef. - by rewrite assocs0. rewrite assocsPtUn // map_cons /=. case: eqP=>[|_]; first by case: eqP=>// <-<- _ _; apply/InPtUnE=>//; left. case: eqP=>// _ [H1]; rewrite eqSS=>H2. by apply/InPtUnE=>//; right; apply: IH H1 H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)