proposition: Lemma all_der_sum c x i (f:= osum2 c) (b:= fun x i => cnext (card_max (omax c x) i)): ordinalp c -> ordinalp x -> ordinalp i -> all_der f b x i = c *o omega0 ^o i +o x.
proof: Proof. move => oc ox oi0. move: (all_der_sum_aux oc); 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 oprod1r//. move:ly => [i oi si]. move => 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. move:(first_derivation_exten (etc _ liy) na) => eq1. move:(all_der_p14 ha hb oi ox); rewrite - si => <- /=. have oo1:= (OS_pow OS_omega oi). have oo:=(OS_prod2 oc oo1). rewrite (eq1 x ox) (add_fix_enumeration oo ox) si (opow_succ OS_omega oi). by rewrite (oprodA oc oo1 OS_omega). have nf:= (all_der_p6 ha hb oy). have ooy := (OS_pow OS_omega oy). have ov := OS_prod2 oc ooy. have ng:= (osum_normal ov). apply:(sincr_ofs_exten (proj1 nf) (proj1 ng)) => x ox. set g := all_der (osum2 c) b. set s := g x y. have os: ordinalp s by apply:(OS_all_der ha hb). case (ozero_dichot oc) => cp. by exists s => //;rewrite cp oprod0l (osum0l os). move:(normal_ofs_compose (oprod_normal cp) oopow_normal). move => [sa sb]; move: (sb y ly) => /=. set F := fun_image _ _. have osF: (ordinal_set F). move => t /funI_P [i iy ->]; apply:(ofs_sincr sa (Os_ordinal oy iy)). have ub: ordinal_ub F s. move => t tF; move:(osF _ tF); move /funI_P: tF => [i iy ->] ot. have liy: i <o y by apply/(oltP oy). move:(all_der_p7 ha hb ox liy). by rewrite (etc _ liy s os) -/g -/s; move => <-;apply: osum_Mle0. move:(ord_ub_sup os ub) => pa pb; rewrite - pb in pa. by move:(odiff_pr pa) => [ra rb]; exists (s -o c *o omega0 ^o y). set g := all_der (osum2 c) b. set a := c *o omega0 ^o y +o x. have yp: \0o <o y by move/limit_ordinal_P:ly => [p2 p3]. have osa:=(OS_sum2 ov ox). have hc: (forall i, i <o y -> all_der (osum2 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_prod2 oc ooi. by rewrite /a (osumA ow ov ox) - (oprodD ooi ooy oc) (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)