proposition: Lemma ord_induction_p21a x y: OIax1b u w0 g -> u <=o x -> y <o omega0 -> (g (w0 x) x) +o y <=o (f x (osucc y)).
proof: Proof. move => ax22 ux; move /olt_omegaP; move: (ax22) => [ax1 ax2]. have ox:= proj32 ux. have ow:= (proj32 (proj32 ax1 _ ux)). move: y; apply: Nat_induction. rewrite osucc_zero osum0r //; rewrite fv ord_induction_y1; fprops. move=> n nN hrec. rewrite (succ_of_nat nN). have on: ordinalp n by apply: OS_cardinal; fprops. move: (olt0S on) => le1. rewrite (ord_induction_p13 fv ax22 ux (proj32_1 le1)). move: (proj33 ax1 _ _ (ord_induction_p41 fv ax1 ux le1) ux) => le2. rewrite - osum2_succ //; apply /oleSltP; exact: (ole_ltT hrec le2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)