proposition: Lemma worder_invariance r r': r \Is r' -> worder r -> worder r'.
proof: Proof. move=> [f [or or' [bf sf tf] sif]] wor. apply:(worder_prop_rev or') => // x xsr [y yx]. set A := Vfs (inverse_fun f) x. have bif := (inverse_bij_fb bf). have fi:= (proj1 (proj1 bif)). have sxt: (sub x (target f)) by rewrite tf. have sxs: (sub x (source (inverse_fun f))) by aw. have sx :source f = (target (inverse_fun f)) by aw. have Asx: sub A (substrate r). rewrite - sf sx; apply: sub_trans (dirim_S sxs) (Imf_Starget fi). have neA: (nonempty A). exists (Vf (inverse_fun f) y); apply /(Vf_image_P fi sxs); ex_tac. move: (worder_prop wor Asx neA) => [z zA zle]. move: (zA) => /(Vf_image_P fi sxs) [u ux Wu]. ex_tac; move =>// v vx. have utx: inc u (target f) by apply: sxt. have uW :=inverse_V bf utx. have vt: inc v (target f) by apply: sxt. set v':= Vf (inverse_fun f) v. have vA: inc v' A by apply /(Vf_image_P fi sxs); ex_tac. rewrite - (inverse_V bf vt) - uW - sif. - by rewrite -Wu; move:(zle _ vA). - rewrite sx; fprops. - rewrite sx; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)