proposition: Lemma ummono_ltP f : reflect (um_mono_ltE f) (um_mono f).
proof: Proof. case: ummonoP=>M; constructor; last first. - by move=>N; elim: M=>x x' y y' X1 X2 /N; apply. move=>x x' y y' X1 X2. move: (M _ _ _ _ X1 X2) (M _ _ _ _ X2 X1)=>O1 O2. split=>// N; case: ordP=>// Y1. - by move/O2: Y1; case: ordP N. by move/eqP: Y1=>?; subst x'; rewrite (In_fun X1 X2) irr in N. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)