proposition: Lemma ummonoP f : reflect (um_mono_lt f) (um_mono f).
proof: Proof. rewrite /um_mono/um_mono_lt/range. apply/(equivP idP); elim/um_indf: f=>[||k v f IH W P]. - by rewrite assocs_undef; split=>// _ ???? /In_undef. - by rewrite assocs0; split=>// _ ???? /In0. rewrite assocsPtUn ?(order_path_min (@trans _) P) //=; split=>H; last first. - rewrite path_min_sorted; first by apply/IH=>??????; apply: H; apply/InR. apply/allP=>x /mapP [[y w]] /mem_seqP/In_assocs X ->. by apply: H (path_mem (@trans K) P (In_dom X)); [apply/InPtUnL|apply/InR]. move=>x x' w w'; rewrite !InPtUnE //. case=>[[->->]|H1]; case=>[[->->]|H2]; first by rewrite irr. - suff: w' \in [seq i.2 | i <- assocs f] by move/(path_mem (@trans V) H). by move/In_assocs/mem_seqP: H2=>H2; apply/mapP; exists (x',w'). - by move/In_dom/(path_mem (@trans K) P): H1; case: ordP. by move/path_sorted/IH: H; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)