proposition: Lemma ord_induction_p13 x y: OIax1b -> u <=o x -> ordinalp y -> f x (osucc y) = g (f x y) x.
proof: Proof. move=> [ax1 ax2] ux oy. move: (OS_succ oy) => osy. have ysy:= oltS oy. apply: oleA; last by apply: ord_induction_p7. have syp: \0o <o osucc y by apply /oltSleP; apply: ole0x. rewrite fv (ord_induction_yp w0 g x syp) -fv. apply: ord_ub_sup. by apply:(ord_induction_p6 ax1 ux oy). move => t /funI_P [s zsa ->]. case /setU1_P: zsa; last first. by move => ->; apply:oleR; apply:ord_induction_p6. move => /(oltP oy) => sy. have ox:= (proj32 ux). wlog: s sy / \0o <o s => sp. have [aux _]: g (f x \0c) x <o g (f x \1c) x. rewrite fv ord_induction_y0 ord_induction_y1. apply: (proj33 ax1 _ _ _ ux); exact: (oleT ux (proj32 ax1 _ ux)). case: (ozero_dichot (proj31_1 sy)); last by apply:sp. move ->; case: (oone_dichot sy)=> yp; first by rewrite yp. apply: (oleT aux (sp _ yp olt_01)). move: (ord_induction_p41 ax1 ux sp) => pa. apply: ax2 => //; [exact (proj1 (ord_induction_p8 ax1 ux sy))| fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)