proposition: Lemma all_der_prod c x i (f:= oprod2 c) (b:= fun x i => cnext (card_max (omax c x) i)): \0o <o c -> ordinalp x -> ordinalp i -> all_der f b x i = c ^o (omega0 ^o i) *o x.
proof: Proof. move => cp ox oi0. have oc:= proj32_1 cp. move: (all_der_prod_aux cp); rewrite -/b; move => [ha hb]. pose p i := forall x, ordinalp x -> all_der f b x i = c ^o (omega0 ^o i) *o x. move: x ox; rename i into i0. apply: (least_ordinal2 (p := p)) oi0 => y oy etc. case: (ordinal_limA oy) => ly. move => x ox; rewrite ly (all_der_p2 ha hb ox) opowx0 opowx1 //. move:ly => [i oi si] x ox. have liy: i <o y by rewrite si;apply:oltS. have na: normal_ofs ((all_der f b)^~ i) by apply: all_der_p6. have eq1:= (first_derivation_exten (etc _ liy) na). move:(all_der_p14 ha hb oi ox); rewrite - si => <- /=. have oo1:= (OS_pow OS_omega oi). have oo:= (opow_pos cp oo1). rewrite (eq1 x ox) (mult_fix_enumeration oo ox) si (opow_succ OS_omega oi). by rewrite (opow_prod oc oo1 OS_omega). have nf:= (all_der_p6 ha hb oy). have ooy := (OS_pow OS_omega oy). have ov := opow_pos cp ooy. have ng:= (oprod_normal ov). apply:(sincr_ofs_exten (proj1 nf) (proj1 ng)) => x ox. set g := all_der (oprod2 c) b. set s := g x y. have os: ordinalp s by exact:(OS_all_der ha hb ox oy). case: (ord2_trichotomy oc) => c2. by move: cp => [];rewrite c2. by exists s => //; rewrite c2 opow1x (oprod1l os). case: (oquoremP os ov); set q := oquo _ _; set r := orem _ _=> oq or sv rp. have op1:= (proj32_1 rp). have op2:= (OS_prod2 op1 oq). case: (ozero_dichot or) => snz. by exists q => //; rewrite sv snz (osum0r op2). have pc: forall i, i <o y -> c ^o (omega0 ^o i) *o r = r. move => i iy. have oi:= proj31_1 iy. have ooi:= (OS_pow OS_omega oi). have op3 := (OS_pow oc ooi). move:(all_der_p7 ha hb ox iy). rewrite (etc _ iy s os) -/g -/s sv (oprodD op2 or op3). rewrite (oprodA op3 op1 oq) - (opow_sum oc ooi ooy) (ord_negl_p4 iy) => h. exact: (osum2_simpl (OS_prod2 op3 or) or op2 h). move:(normal_ofs_compose (opow_normal c2) oopow_normal). move => [sa sb]; move: (sb y ly) => /=. set F := fun_image _ _. have osF: (ordinal_set F). move => t /funI_P [i /(Os_ordinal oy) iy ->]; apply:(ofs_sincr sa iy). have ub: ordinal_ub F r. move => t tF; move:(osF _ tF); move /funI_P: tF => [i iy ->] ot. move /(oltP oy): iy => /pc <-. apply: oprod_Mle1 => //. move => pb; case:(oltNge rp); rewrite pb; exact:(ord_ub_sup or ub). set g := all_der (oprod2 c) b. set a := c ^o (omega0 ^o y) *o x. have ovv:= (proj32_1 ov). have yp: \0o <o y by move/limit_ordinal_P:ly => [p2 p3]. have osa: ordinalp a by move: (OS_prod2 ovv ox). have hc: (forall i, i <o y -> all_der (oprod2 c) b a i = a). move => i iy; rewrite (etc _ iy a osa). have oi:=proj31_1 iy. have ooi := (OS_pow OS_omega oi). have ow := OS_pow oc ooi. by rewrite /a (oprodA ow ovv ox) -(opow_sum oc ooi ooy) (ord_negl_p4 iy). by move:(all_der_p8 ha hb osa yp hc) => [u ua ub]; exists u. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)