proposition: Lemma worder_image r r' f A: order_isomorphism f r r' -> sub A (substrate r) -> let oa := (induced_order r A) in let ob := (induced_order r' (Vfs f A)) in worder oa -> (worder ob /\ ordinal oa = ordinal ob).
proof: Proof. move=> isf Asr oa ob wo1. move: (isf) => [o1 o2 [bf sf tf] isfo]. have ff: function f by fct_tac. have sAs: sub A (source f) by ue. have pa: sub (Vfs f A) (substrate r'). move => t /(Vf_image_P ff sAs) [u uA ->]; rewrite - tf; Wtac. move: (iorder_osr o2 pa) => [oob sob]. move: (bf) => [injf _]. move: (restriction1_fb injf sAs) => br. have sr1: (source (restriction1 f A)) = A by rewrite /restriction1 ; aw. have aux: forall x, inc x A -> inc (Vf f x) (Vfs f A). move => x xA; apply /(Vf_image_P ff sAs); ex_tac. have abis: oa \Is ob. exists (restriction1 f A); split;fprops; first split => //. rewrite /oa sr1 iorder_sr//. by rewrite /ob /restriction1 iorder_sr //; aw. hnf;rewrite sr1; move=> x y xA yA. move: (sAs _ xA) (sAs _ yA) => xs ys. rewrite restriction1_V // restriction1_V //. by split;move / iorder_gleP => [qa qb qc]; apply /iorder_gleP;split => //; try (apply: aux =>//); apply/(isfo _ _ xs ys). suff soob: worder ob by split => //; apply: ordinal_o_isu1. split => //. move: wo1 => [ _ ]. rewrite iorder_sr // iorder_sr // => wo1. move => x xi nex; rewrite iorder_trans //. set z:= Vfs (inverse_fun f) x. move: (inverse_bij_fb bf) => ibf. have fif: function (inverse_fun f) by fct_tac. have sxt: sub x (target f) by apply: (sub_trans xi); apply: fun_image_Starget1. have sxt1: sub x (source (inverse_fun f)) by aw. have sxs: sub x (substrate r') by ue. have nez: nonempty z. move: nex => [w wx]; exists (Vf (inverse_fun f) w). apply /(Vf_image_P fif sxt1); ex_tac. have za: sub z A. move=> t /(Vf_image_P fif sxt1) [u ux ->]. move: (xi _ ux) => /(Vf_image_P ff sAs); move=> [v vA ->]. by rewrite (inverse_V2 bf (sAs _ vA)). move: (wo1 _ za nez); rewrite iorder_trans //; move => [y []]. have zr: sub z (substrate r) by rewrite - sf; apply: sub_trans sAs. rewrite /has_least /least iorder_sr // iorder_sr //. move /(Vf_image_P fif sxt1) => [z1 z2 ->] yl;exists z1; split => //. move => a ax; apply /iorder_gleP => //. set b := Vf (inverse_fun f) a. have bz: inc b z by apply /(Vf_image_P fif sxt1); ex_tac. have atf: inc a (target f) by apply sxt. have z1tf: inc z1 (target f) by apply sxt. have qa: inc (Vf (inverse_fun f) z1) (source f) by apply: inverse_Vis. have qb: inc (Vf (inverse_fun f) a) (source f) by apply: inverse_Vis. move: (yl _ bz) => le1; move: (iorder_gle1 le1). rewrite /b isfo // (inverse_V bf z1tf) // (inverse_V bf atf) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)