proposition: Lemma normal_ofs_existence1 (p:fterm) a u: (forall x, ordinalp x -> x <o p x) -> (forall x y, x <=o y -> p x <=o p y) -> ordinalp a -> ordinalp u -> exists f, [/\ normal_ofs1 f u, f u = a & (forall x, u <=o x -> f (osucc x) = p (f x)) ].
proof: Proof. move => ha hb oa ou. move: (normal_ofs_existence ha hb oa). set g := transdef_ord _; move => [ga gb gc]. have leuu:= oleR ou. pose f x := g (x -o u); exists f; split; last first. - move => x ux; move:(odiff_pr ux) =>[od dp]. rewrite /f - (gc _ od). rewrite {1} dp. rewrite (osum2_succ) // odiff_pr1 //; apply:(OS_succ od). - by rewrite - gb /f (odiff_wrong leuu). have ra:=(normal_ofs_equiv2 OS0 ga). have rb: \0c <=o u -o u by rewrite (odiff_wrong leuu); apply: (oleR OS0). have rc := (odiff_normal ou). exact:(normal_ofs_compose1 (g:= (odiff^~ u) ) OS0 ou rb ra rc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)