proposition: Lemma In_rangev (h : Ur) (x : aT) : ocancel f g -> pcancel g f -> x \In range (omapv f h : Ua) <-> g x \In range h.
proof: Proof. move=>O P; rewrite !In_rangeX; split; case=>k H; exists k; by [rewrite -In_omapV | rewrite In_omapV]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)