proposition: Lemma ord_induction_p10 x: OIax1 -> u <=o x -> normal_ofs (f x).
proof: Proof. move=> ax1 ux; split. move => y y'; apply:(ord_induction_p8 ax1 ux). move => a la. rewrite fv (ord_induction_yp w0 g x (limit_pos la)) -fv. apply: ord_sup_2cofinal; split => b /funI_P [z za ->]. move: la => [pa pb pc]; move: (pc _ za) => sza. exists (f x (osucc z)); first by apply/funI_P;ex_tac. apply: (ord_induction_p7 ax1 ux); apply: (oltS (Os_ordinal pa za)). move: la => [pa pb pc]. have oz:=(Os_ordinal pa za). exists (g (f x z) x); first by apply/funI_P; exists z. case: (ozero_dichot oz) => aa. rewrite aa fv ord_induction_y0; exact (proj1 (proj31 ax1 _ ux)). exact (proj1 (proj33 ax1 _ _ (ord_induction_p41 ax1 ux aa) ux)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)