proposition: Lemma In_mono_range k f1 f2 : valid (f1 \+ f2) -> um_mono (f1 \+ f2) -> k \in range f1 -> k \in range f2 -> false.
proof: Proof. move=>W M /mem_seqP/In_rangeX [v1 H1] /mem_seqP/In_rangeX [v2 H2]. have H1' : (v1, k) \In f1 \+ f2 by apply/InL. have H2' : (v2, k) \In f1 \+ f2 by apply/InR. rewrite -{v2 H1' H2'}(In_mono_fun M H1' H2') in H2. move/In_dom: H2; move/In_dom: H1=>H1. by rewrite (negbTE (dom_inNL W H1)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)