proposition: Lemma all_der_pow_aux (b:= fun x i => cnext (card_max x i)): normal_ofs oopow /\ all_der_bound oopow b.
proof: Proof. split; first by exact: oopow_normal. move => x i ox oi. move: (omax_p3 ox oi) => [sa sb sc]; split => //. by exists (card_max x i). move => t tb; apply/cnext_pow => //. apply/(cnextP (proj1 sa)); split; fprops. apply:ocle1 (proj2 (omax_p1 (OS_omax ox oi) OS_omega)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)