proposition: Lemma normal_ofs_compose1 f fb g gb: ordinalp fb -> ordinalp gb -> fb <=o g gb -> normal_ofs1 f fb -> normal_ofs1 g gb -> normal_ofs1 (f \o g) gb.
proof: Proof. move => ofb ogb le1 [sa pa] [sb pb]. have aux: forall z, gb <=o z -> fb <=o g z. move => z zh; apply: (oleT le1). have oug:= (oleR (ofs_sincru sb zh)). case: (equal_or_not gb z); [move => -> // | move =>h]. exact (proj1 (sb gb z (oleR ogb) (conj zh h))). split. move => u v ha uv /=. by move: (sb _ _ ha uv); apply: sa; apply: aux. move => X Xp neX /=; rewrite - (pb _ Xp neX). set Y := (fun_image X g). have sc:(forall x, inc x Y -> fb <=o x). by move => x /funI_P [z /Xp zx ->]; apply: aux. have nY: nonempty Y by move: neX => [t tX]; exists (g t); apply /funI_P; ex_tac. rewrite -(pa _ sc nY); congr union; set_extens t; move/funI_P => [z za ->]. apply/funI_P; exists (g z)=> //;apply /funI_P; ex_tac. move/funI_P: za => [u tX ->]; apply/funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)