proposition: Lemma ummono_leP f : um_mono f -> um_mono_leE f.
proof: Proof. move/ummonoP=>M x x' y y' X1 X2. move: (M _ _ _ _ X1 X2) (M _ _ _ _ X2 X1)=>O1 O2. rewrite /oleq (eq_sym x) (eq_sym y). case: ordP=>Y1; case: ordP=>Y2 //=. - by move/O2: Y1; rewrite (eqP Y2) irr. - by move/O2: Y1; case: ordP Y2. - by rewrite (eqP Y1) in X2; rewrite (In_fun X1 X2) irr in Y2. by move/O1: Y1; case: ordP Y2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)