proposition: Lemma fsincr_wor_prop r X f: worder r -> sub X (substrate r) -> order_isomorphism f r (induced_order r X) -> forall x, inc x (substrate r) -> gle r x (Vf f x).
proof: Proof. move => wor ser [_ _ [/proj1/proj1 bf sf tf] ff]. case: (worder_prop2 (fun x => gle r x (Vf f x)) wor) => // - [a [asr fa ap]]. case: fa. have H t: inc t (source f) -> inc (Vf f t) X. rewrite - (iorder_sr (proj1 wor) ser) - tf => xs. Wtac. have asf: inc a (source f) by ue. have bX := H _ asf. case: (total_order_pr2 (worder_total wor) (ser _ bX) asr) => // /ap aux. move:(ser _ bX);rewrite - sf => bsf; move: (H _ bsf) => vvX. by apply/(ff a (Vf f a) asf bsf); apply/iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)