proposition: Lemma first_derivation_p4 (f: fterm) C (E:= cnext C) (f' := first_derivation f) (F := Zo E (fun z => f z = z)): infinite_c C -> normal_ofs f -> (forall x, inc x E -> inc (f x) E) -> order_isomorphism (Lf f' E F) (ordinal_o E) (ole_on F).
proof: Proof. move => iC nf fse;move: (iC) => [cC _]. move:(cnext_pr1 cC); rewrite -/E; move=> [pa pb pc]. move: (iclosed_fixpoints nf)=> pab'. move: (ordinals_col_p2 pab') => nf'. set p := (fun z => ordinalp z /\ f z = z). have pc': forall x, p x -> ordinalp x by move=> x []. move: (ordinals_col_p1 pc' (proj2 pab')). have -> : ordinalsf p = f' by []. move => [q1 q2 q3 q4 [q5 q6]]. move: (proj1 pa) => oe. have oes:= (Os_ordinal oe). set g := Lf f' E F. have sa: forall a b, inc b E -> a <o b -> inc a E. move => a b /(oltP oe) ha hb; apply/(oltP oe); apply:olt_ltT hb ha. have lfa: lf_axiom f' E F. move => x xE; move: (oes _ xE) => ox; move:(q1 _ ox) => [_ aa]. apply: Zo_i => //; clear aa. move: x ox xE;apply:least_ordinal2 => x ox xp xE. have ozz:= (oes _ xE). have ell: forall t, t <o x -> inc (f' t) E. move => t ltx; apply: (xp _ ltx (sa _ _ xE ltx)). have H:= (next_fix_point_small iC nf fse). case: (ordinal_limA ox). move => ->; rewrite /f' (first_derivation_p1 nf); apply: H. apply cnextP => //; split;rewrite ? (card_card CS0); fprops. apply(cle0x cC). move => [t ot te]; rewrite te. rewrite /f' (first_derivation_p3 nf ot); apply: H. by apply:(cnext_succ iC); apply: ell; rewrite te; apply: oltS. move => lz; move: (proj2 nf' _ lz). set w := ordinalsf _ ; have -> : w = f' by []; clear w. move => ->; apply: (cnext_sup iC). move /(cnextP cC): xE => [_]; apply: cleT. exact: (fun_image_smaller x f'). by move => t /funI_P [u /(oltP ox) uz ->]; apply:ell. split. - apply: ordinal_o_or. - apply: order_from_rel; apply:ole_order_r. - split. + apply: lf_bijective. - done. - move => u v /oes ou /oes ov sv. by case: (oleT_ell ou ov) => // /q4 []; rewrite sv. - move => y /Zo_P [ye yv]; move: (q2 _ (conj (oes _ ye) yv)) => [a a1 a2]. exists a => //; move: (osi_gex q4 a1); rewrite - a2. move /(oltP oe): ye => ha hb; apply/(oltP oe); apply:(ole_ltT hb ha). + by rewrite ordinal_o_sr /g; aw. + by rewrite graph_on_sr /g ; aw; trivial => a /Zo_P [/oes /oleR oa _]. - hnf;rewrite /g;aw; move => x y xE yE; rewrite !LfV//; split. move /sub_gleP => [_ _ xy]; apply /graph_on_P1; split; fprops. apply: q3; split; fprops. move /graph_on_P1 => [_ _] /(q5 _ _ (oes _ xE) (oes _ yE)) [_ _ xy]. by apply /sub_gleP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)