proposition: Lemma sorted_range_inverse f : valid (inverse f) -> sorted ord (range f) -> sorted ord (range (inverse f)).
proof: Proof. move=>W /ummonoP X; apply/ummonoP=>v v' k k'. move/(In_inverse _ _ W)=>H1 /(In_inverse _ _ W) H2. apply: contraTT; case: ordP=>//= E _; first by case: ordP (X _ _ _ _ H2 H1 E). by move/eqP: E H2=>-> /(In_fun H1) ->; rewrite irr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)