proposition: Lemma all_der_p4 x y i: ordinalp i -> x <o y -> [/\ inc x (cnext (union (Zo (b y i) cardinalp))), g x i = all_der_aux f (b y i) x i & g y i = all_der_aux f (b y i) y i].
proof: Proof. move => oi xy. move: (xy) => [[ox oy _] _]. have [sa sb sc sd se]:= (all_der_bound_prop oy oi bf). rewrite sd in sb sc se. have xe: inc x (cnext (union (Zo (b y i) cardinalp))). have ose:= (proj1 (CS_cnext (proj1 sa))). move/(oltP ose): sb => lt1. apply/(oltP ose); apply: olt_ltT xy lt1. rewrite (all_der_p1 sa xe sc se); split => //. rewrite /g /all_der - sd//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)