proposition: Lemma uniq_range_inverse f : uniq (range (inverse f)).
proof: Proof. case W : (valid (inverse f)); last first. - by move/invalidE: (negbT W)=>->; rewrite range_undef. rewrite /range map_inj_in_uniq. - by apply: (@map_uniq _ _ fst); rewrite -assocs_dom; apply: uniq_dom. case=>x1 x2 [y1 y] /= H1 H2 E; rewrite {x2}E in H1 *. move/mem_seqP/In_assocs/(In_inverse _ _ W): H1=>H1. move/mem_seqP/In_assocs/(In_inverse _ _ W): H2=>H2. by rewrite (In_fun H1 H2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)