proposition: Lemma all_der_p14 i: ordinalp i -> first_derivation (g ^~i) =1o g ^~(osucc i).
proof: Proof. move=> oi. have sa:= (first_derivation_p0 (all_der_p6 oi)). have sb:= (all_der_p6 (OS_succ oi)). move: (proj1 sa)(proj1 sb) => ia ib. move: (first_derivation_p (all_der_p6 oi))=> [sc sd]. apply:sincr_ofs_exten => // x ox. move:(sc _ ox); set y := first_derivation (g^~ i) x => h. have snz:= (olt0S oi). have oxx:=(ofs_sincr ia ox). apply: all_der_p8 => // j jsi. case (equal_or_not j i) => eji; first by rewrite eji. have ji: j <o i by move /oltSleP: jsi => h1. by move: (all_der_p7 oxx ji); rewrite -/y h. have oy:=(OS_all_der ox (OS_succ oi)). have se:= (all_der_p7 ox (oltS oi)). exact: (sd _ oy se). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)