proposition: Lemma all_der_p3 x i: ordinalp x -> ordinalp i -> inc (g x i) (b x i).
proof: Proof. move => ox oi. have [sb sc sd se sf]:= (all_der_bound_prop ox oi bf). have sa:= (all_der_bound_prop2 ox oi). rewrite se in sa. move:(many_der_ex sb sa) => [_ _ _ _ [_ _ pg _]]. rewrite se in sd. move: (pg _ sd); rewrite - se; move => [[p1 p2 p3] _ _]. rewrite -p3 /g/all_der/all_der_aux; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)