proposition: Lemma worder_decreasing_finite_orig r r' (f:fterm): worder r -> worder r' -> (forall i, inc i (substrate r) -> inc (f i) (substrate r')) -> (forall i j, glt r i j -> glt r' (f j) (f i)) -> finite_set (substrate r).
proof: Proof. move=> wor wor' ta finc; move: (proj1 wor') => or'. move: Nat_order_wor=> [wob bsr]. case: (isomorphism_worder3 wob wor); last first. move => [x]; rewrite bsr; move => xn [g [pa pb]]. have ss:=(@sub_segment Nat_order x). rewrite (iorder_sr (proj1 wob) ss) (segment_Nat_order xn) => fp _. have cc:cardinal (Nint x)= cardinal (substrate r) by apply/card_eqP; exists g. by rewrite /finite_set - cc; apply: finite_Nint. move =>[g [sr isg]]. have gsi:=(order_morphism_sincr isg). move: isg => [or _ [fg sg tg] incfg]. have sg1: source g = Nat by rewrite sg bsr. move: sr => [sr1 _]. set Y := fun_image (Imf g) f. have Ysr: sub Y (substrate r'). move => t /funI_P [z /(Imf_P fg) [x1 x1g x1p] ->]; apply: ta. rewrite x1p; apply: sr1; Wtac. have yi n: natp n -> inc (f (Vf g n)) Y. by move => nN;apply/funI_P;exists (Vf g n)=> //;Wtac; rewrite sg1. have neY: nonempty Y by exists (f (Vf g \0c)); apply (yi _ NS0). move:(worder_prop wor' Ysr neY) => [y /funI_P [z za zb] yb]. move/(Imf_P fg): za => [n nN np]; rewrite sg1 in nN. have lt1: glt Nat_order n (csucc n). move:(cltS nN) => [qa qb]. split => //; apply /Nat_order_leP; split => //; apply: (NS_succ nN). move:(finc _ _ (gsi _ _ lt1)); rewrite - np - zb => lt2. have /yb lt3: inc (f (Vf g (csucc n))) Y by apply:yi; apply:NS_succ. order_tac. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)