proposition: Lemma all_der_sum_aux c (f:= osum2 c) (b:= fun x i => cnext (card_max (omax c x) i)): ordinalp c -> normal_ofs f /\ all_der_bound f b.
proof: Proof. move => oc; split; first by apply:osum_normal. move => x i ox oi. have om:= (OS_omax oc ox). move: (omax_p3 om oi); rewrite -/(card_max _ _) -/(b x i). move => [sa sb sc]. have ec: exists2 C, infinite_c C & b x i = cnext C. by exists (card_max (omax c x) i). move:(omax_p1 oc ox) => [sd se]. have ha: ordinalp (b x i) by exact: (proj1 (CS_cnext (proj1 sa))). move/(oltP ha): sb => sf. have pa: inc x (b x i) by apply /(oltP ha); apply: (ole_ltT se sf). have pb: inc c (b x i) by apply /(oltP ha); apply: (ole_ltT sd sf). have pc: forall y, inc y (b x i) -> inc (c +o y) (b x i). move => y ye;apply: cnext_sum => //. split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)