proposition: Lemma ord_induction_p21b x: OIax1b u w0 g -> u <=o x -> x +o omega0 <=o (f x omega0).
proof: Proof. move=> ax ux; move: (ax) => [ax1 ax2]. have ox:= proj32 ux. have ol:=omega_limit. rewrite (proj2 (ord_induction_p10 fv ax1 ux) _ ol)(proj2 (osum_normal ox) _ ol). have ot: ordinal_set(fun_image omega0 (f x)). by apply:Os_funI => w /(OS_nat) ;apply: (ord_induction_p5 fv ax1). apply: ord_ub_sup. - by apply:OS_sup. - move => t /funI_P [w wi ->]. move: (proj33 ol _ wi) => so. move/(oltP OS_omega):wi =>h; move: (ord_induction_p21a ax ux h) => l1. apply:(oleT (oleT (osum_Mleeq (proj32 ax1 _ ux) (proj31_1 h)) l1)). apply: ord_sup_ub => //; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)