proposition: Lemma ummono_inj_find f : um_mono f -> {in dom f & predT, injective (fun x => find x f)}.
proof: Proof. move/ummono_leP=>H k1 k2 /In_domX [x1 F1] _ E. have /In_domX [x2 F2] : k2 \in dom f. - by case: dom_find F1 E=>// -> /In_find ->. move/In_find: (F1) E=>->; move/In_find: (F2)=>-> [?]; subst x2. move: (H _ _ _ _ F1 F2) (H _ _ _ _ F2 F1); rewrite orefl=>{H} H1 H2. case: (equivP idP H1) (@oantisym K k1 k2)=>// _. by case: (equivP idP H2)=>// _; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)