proposition: Lemma cofinal_image r r' f x: order_isomorphism f r r' -> cofinal r x -> cofinal r' (Vfs f x).
proof: Proof. move=> [o1 o2 [bf sf tf] isf] [xsr cx]. have ff: function f by fct_tac. have xsf: sub x (source f) by ue. split. move=> t /(Vf_image_P ff xsf) [u ux ->]; rewrite - tf; Wtac. rewrite - tf; move => y yt; move: (bij_surj bf yt) => [z zf ->]. rewrite sf in zf; move: (cx _ zf) => [t tx ty]. exists (Vf f t); first by apply/(Vf_image_P ff xsf); ex_tac. rewrite -isf //; [ ue | by apply: xsf]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)