proposition: Lemma add_fix_enumeration a: ordinalp a -> first_derivation (osum2 a) =1o (osum2 (a *o omega0)).
proof: Proof. move => oa. set b := a *o omega0. have ob: ordinalp b by apply: (OS_prod2 oa OS_omega). move: (osum_normal oa) (osum_normal ob) => npa npb. have pa:= (iclosed_fixpoints npa). have na:=(ordinals_col_p2 pa). apply:(normal_ofs_uniqueness (p:= fun z => z+o \1o)) => //. move => x ox. move: (iclosed_col_fs pa ox). set u:= ordinalsf _ x; set v := ordinalsf _ (osucc x). move => [sa [ou sb] _ sc]. move: (oltS ou) => h. rewrite osucc_pr //; apply: oleA; last by apply /oleSltP. by apply: (sc _ _ h); split; [ fprops | rewrite - (osum2_succ oa ou) sb]. move => x ox; rewrite - osucc_pr // osumA //; fprops. rewrite osum0r //. rewrite (first_derivation_p1 npa) /the_least_fixedpoint_ge. move: (induction_defined_pr (osum2 a) \0o). set g := induction_defined _ _; move => [sg [fg sjg g0 gn]]. rewrite sg in sjg. move: NS0 => bs0. have gnn: forall n, natp n -> Vf g n = a *o n. apply: Nat_induction; first by rewrite oprod0r. move => n nb h. rewrite (gn _ nb) h (oprod2_nsucc oa (OS_nat nb)) (osum2_2int NS1 nb). by rewrite (Nsucc_rw nb) csumC. case: (ozero_dichot oa) => ap. suff: (target g) = singleton \0o by move => ->; rewrite setU_1 /b ap oprod0l. apply: set1_pr; first by rewrite - g0; Wtac; rewrite sg. by move => z /sjg [x /gnn xsg ->]; rewrite xsg ap oprod0l. move: (oprod_normal ap) => /normal_ofs_equiv1 [ha hb]. have ->: (target g) = (fun_image Nat (oprod2 a)). set_extens t; first by move/sjg => [x xa ->]; apply /funI_P; ex_tac. move /funI_P => [z zN ->]; rewrite - (gnn _ zN); Wtac. have bns:(forall x, natp x -> \0o <=o x) by move => x /OS_nat /ole0x. have nex: nonempty Nat by exists \0c; apply: NS0. by rewrite(hb _ bns nex) - [union _]omega_limit0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)