proposition: Lemma valid_inverse f : valid (inverse f) = [&& valid f, uniq (range f) & all C' (range f)].
proof: Proof. elim/um_indf: f=>[||k v f IH W /(order_path_min (@trans K)) P]. - by rewrite inverse_undef !valid_undef. - by rewrite inverse0 !valid_unit range0. rewrite inversePtUn W //= rangePtUnK // validPtUn /=. rewrite IH (validR W) /=; bool_congr; rewrite andbC -!andbA. rewrite andbC [in X in _ = X]andbC. case X1 : (uniq (range f)) IH=>//=. case X2 : (all C' (range f))=>//=. by rewrite (validR W)=>/dom_inverse ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)