proposition: Lemma mult_fix_enumeration a: \0o <o a -> first_derivation (oprod2 a) =1o (oprod2 (a ^o omega0)).
proof: Proof. move => ap. set b := a ^o omega0. have oa:= proj32_1 ap. have ob: ordinalp b by apply: (OS_pow oa OS_omega). have bp: \0o <o b by apply: opow_pos => //; apply: OS_omega. move: (oprod_normal ap) (oprod_normal bp) => npa npb. move: (iclosed_fixpoints npa) => pa. move:(ordinals_col_p2 pa) => na. have w0: first_derivation (oprod2 a) \0o = b *o \0o. rewrite oprod0r. have h: ordinalp \0o /\ a *o \0o = \0o by split; [ fprops| apply: oprod0r]. by move: (iclosed_col_f0 pa) => [_ sc]; move: (sc _ h) => /ole0. apply:(normal_ofs_uniqueness (p:= fun z => z+o b)) => //; last first. by move => x ox; apply: oprod2_succ. move => x ox. move: (iclosed_col_fs pa ox); rewrite /first_derivation. set u:= ordinalsf _ x; set v := ordinalsf _ (osucc x). move => [sa [ou sb] [ov sc] sd]. move: (oprod_fix2 ap ou sb) => [y oy uv]. move: (oprod_fix2 ap ov sc) => [z oz vv]. move: (OS_succ oy) => osu. move: (conj (OS_prod2 ob osu) (oprod_fix1 ap osu)) => ea. move:(oprod_Meqlt (oltS oy) bp); rewrite - uv => eb. move: (sd _ ea eb); rewrite uv - (oprod2_succ ob oy) vv -/b => h1. ex_middle h2. rewrite uv vv in sa;move: (oprod_Meqltr oy oz ob sa) => /oleSltP l1. case: (oleNgt l1 (oprod_Meqltr oz osu ob (conj h1 h2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)