proposition: Lemma range_inverse f : valid (inverse f : U') -> range (inverse f) =i dom f.
proof: Proof. elim/um_indf: f=>[||k v f IH W P]. - by rewrite inverse_undef valid_undef. - by rewrite inverse0 range0 dom0. rewrite inversePtUn // => W' x. rewrite rangePtUn inE W' domPtUn inE W /=. by case: eqP=>//= _; rewrite IH // (validR W'). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)