proposition: Lemma mem_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. by move=>O P; apply/idP/idP; move/mem_seqP/(In_rangev _ _ _ O P)/mem_seqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)