proposition: Lemma ord_induction_p20 u w0 g b (f:= ord_induction_defined w0 g): OIax2 u w0 g -> ordinalp b -> exists2 E, finite_set E & forall y, (inc y E) <-> (exists x, [/\ u <=o x, ordinalp y & f x y = b]).
proof: Proof. move=> axx ob; move: (axx) => [ax1 _ _ _]. have fv: f = ord_induction_defined w0 g by done. pose p x y:= [/\ u <=o x, ordinalp y & f x y = b]. set E := Zo (osucc b) (fun y => exists x, p x y). exists E; last first. move=> y; split; first by move /Zo_P => []. move=> h; apply/Zo_P;split; last (by exact). move: h=> [x [ux oy fb]]; apply /(oleP ob); rewrite - fb. exact: (ord_induction_p9 fv ax1 ux oy). pose the_x y := choose (fun x => p x y). have the_xp: forall y, inc y E -> p (the_x y) y. by move=> y yE; apply choose_pr; move: yE => /Zo_P [_]. pose the_lx y := least_ordinal (fun x => p x y) (the_x y). have the_lxp: forall y, inc y E -> [/\ ordinalp (the_lx y) , p (the_lx y) y & (forall z, ordinalp z -> p z y -> (the_lx y) <=o z )]. move=> y yE; move: (the_xp _ yE) => pv. move: (pv) => [[_ pw _] _ _]. exact:(least_ordinal4 (p:= p ^~y) pw pv). have thex_dec: forall y1 y2, inc y1 E -> inc y2 E -> y1 <o y2 -> (the_lx y2) <o (the_lx y1). move=> y1 y2 /the_lxp [ox1 px1 minx1] /the_lxp [ox2 px2 minx2] y12. case: (oleT_el ox1 ox2) => le1 //. move: px1 px2 => [pa pb pc] [pd pe pf]. move: (ord_induction_p16 fv axx pa le1 (oleR pb)). move: (ord_induction_p8 fv ax1 pd y12); rewrite pc pf => lea lta. case: (oleNgt lta lea). have ose: ordinal_set E by move=> x => /Zo_P [_ [y [_ p3 _]]]. move: (wordering_ole_pr ose). set r:= ole_on E; move => [pd pc]. rewrite -pc; apply: well_ordered_opposite => //. move: pd => [pd pe]. move: (opp_osr pd) => [or1]; rewrite pc => sr1. split; fprops; rewrite /has_least/least sr1 => X XE neX. rewrite iorder_sr; [ | fprops | ue]. set Y := fun_image X the_lx. have neY: nonempty Y . move: neX => [x xE]; exists (the_lx x); apply /funI_P; ex_tac. have osy: ordinal_set Y. move=> x /funI_P [y yx yv]. by move: (the_lxp _ (XE _ yx)); rewrite yv; move=> [p1 _ _]. move: (wordering_ole_pr osy) => [pd1 pc1]. rewrite - pc1 in neY; move: (worder_least pd1 neY) => [y []]. rewrite pc1 => /funI_P [x xX xv] => xv1. exists x; split => //;move => t tX; apply /iorder_gle0P => //. apply /opp_gleP/graph_on_P1;split => //; try apply:XE => //. have aux: inc (the_lx t) Y by apply /funI_P; ex_tac. move: (xv1 _ aux) => /graph_on_P1 [p1 p2 p3]. have ox: ordinalp x by move: (ose _ (XE _ xX)). have ot: ordinalp t by move: (ose _ (XE _ tX)). case: (oleT_el ot ox) => le1 //. by move: (thex_dec _ _ (XE _ xX) (XE _ tX) le1); rewrite - xv => /(oleNgt p3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)