proposition: Lemma image_of_greatest r r' f x: order_isomorphism f r r' -> greatest r x -> greatest r' (Vf f x).
proof: Proof. move => [or or' [sf tf bf] incf] [xs xg]. rewrite - tf in xs. split; first by Wtac; fct_tac. rewrite - bf;move => y /(bij_surj sf) [z zsf ->]. apply/ (incf _ _ zsf xs);apply: xg; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)