proposition: Lemma first_derivation_exten f g : f =1o g -> normal_ofs f -> first_derivation f =1o first_derivation g.
proof: Proof. move => h osf. have osg := (normal_ofs_from_exten h osf). have [sa sb]:=(first_derivation_p osf). have [sc sd] :=(first_derivation_p osg). move: (first_derivation_p0 osf) (first_derivation_p0 osg) => [ia _] [ib _]. apply: (sincr_ofs_exten ia ib). + move => x ox. have ha: ordinalp (first_derivation f x) by apply: ofs_sincr. by apply: sd => //;rewrite - h //;apply: sa. + move => x ox. have ha: ordinalp (first_derivation g x) by apply: ofs_sincr. by apply: sb => //;rewrite h //;apply: sc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)