proposition: Lemma all_der_p5 x y i: ordinalp i -> x <o y -> g x i <o g y i.
proof: Proof. move => oi xy. have [xe v1 v2]:=(all_der_p4 oi xy). have [[ox oy _] _] := xy. have [sa sb sc sd se]:= (all_der_bound_prop oy oi bf). move: (all_der_bound_prop2 oy oi); rewrite sd => sf. rewrite sd in sb sc se. move:(many_der_ex sa sf) => [_ _ _ _ [_ _ ug _]]. move: (ug _ sc) => [ua ub _];move: (ub _ _ xe sb xy). rewrite - sd v1 v2//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)