proposition: Lemma all_der_bound_prop f b x i (E:= b x i) (C := (\csup (Zo E cardinalp))): ordinalp x -> ordinalp i -> all_der_bound f b -> [/\ infinite_c C, inc x E, inc i E, E = cnext C & forall t, inc t E -> inc (f t) E].
proof: Proof. move => ox oi h. move: (h _ _ ox oi) => [sa sb sc sd]. by move: (cnext_pred_more sc) => [sz sf]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)