proposition: Lemma ord_induction_p21c x y: OIax1b u w0 g -> u <=o x -> omega0 <=o y -> x +o y <=o (f x y).
proof: Proof. move=> ax ux oy0; move: (ax) => [ax1 ax2]. have loo:=olt_0omega. have oy1:= proj32 oy0. have ox:= proj32 ux. move: y oy1 oy0; apply: least_ordinal2 => z oz plz loz. case: (ole_eqVlt loz) => h1. by rewrite - h1; apply:ord_induction_p21b. case: (ordinal_limA oz) => H. by move: (olt_0omega); rewrite - H => /(oleNgt loz). move:H=> [t ot tv]; rewrite tv. have lezo: omega0 <=o t by apply /oltSleP; rewrite - tv. have lttz : t <o z by rewrite tv; apply: oltS. have tp:= (olt_leT loo lezo). rewrite - osum2_succ //; apply /oleSltP. rewrite (ord_induction_p13 fv ax ux ot). move: (proj33 ax1 _ _ (ord_induction_p41 fv ax1 ux tp) ux). exact:ole_ltT (plz _ lttz lezo). rewrite (proj2 (osum_normal ox) _ H). set T1 := fun_image _ _. have ot1: ordinal_set T1. apply:Os_funI => w wi; exact : (OS_sum2 ox (Os_ordinal oz wi)). have le1:= (olt_leT loo loz). move: (ord_induction_p5 fv ax1 ux (proj31 H)) => ofo. apply: (ord_ub_sup ofo) => i /funI_P [j jz ->]. have oj:= Os_ordinal oz jz. have fi:forall t, t <o z -> f x t <=o f x z. move => t tz; exact (proj1 (ord_induction_p8 fv ax1 ux tz)). case: (oleT_el OS_omega oj) => cpjo. have jy: j <o z by apply /oltP. by move: (plz _ jy cpjo) => h; apply: (oleT h); apply: fi. apply: (oleT (osum_Meqle (proj1 cpjo) ox)). by apply: (oleT (ord_induction_p21b ax ux)); apply: fi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)