proposition: Lemma In_inverse k v f : valid (inverse f) -> (k, v) \In f <-> (v, k) \In inverse f.
proof: Proof. elim/um_indf: f k v=>[||x w f IH W /(order_path_min (@trans K)) P] k v. - by rewrite inverse_undef valid_undef. - by rewrite inverse0; split=>/In0. move=>W'; rewrite inversePtUn // !InPtUnE //; last by rewrite -inversePtUn. rewrite IH; first by split; case=>[[->->]|]; auto. rewrite !valid_inverse rangePtUnK // (validR W) in W' *. by case/and3P: W'=>_ /= /andP [_ ->] /andP [_ ->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)