proposition: Lemma OS_all_der x i: ordinalp x -> ordinalp i -> ordinalp (g x i).
proof: Proof. move=> ox oi; move: (all_der_p3 ox oi) => h. have [sb _ _ se _]:= (all_der_bound_prop ox oi bf). rewrite se in h. exact: (Os_ordinal (proj1 (CS_cnext (proj1 sb))) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)