proposition: Lemma ord_induction_p4 x y: OIax1 -> u <=o x -> \0o <o y -> x <=o (f x y).
proof: Proof. move=> [_ aw1 ag1] ux0 loy0; ex_middle npy0. move: (least_ordinal5 loy0 npy0 (p:= fun z => x <=o (f x z))) => /=. set z := least_ordinal _ _; move=> [oz z1 npz lpy];case: npz. move: (aw1 _ ux0) => le1. case: (oone_dichot z1) => x3; first by rewrite x3 fv ord_induction_y1. rewrite fv (ord_induction_yp w0 g x z1) - fv /ord_induction_sup. set T:= fun_image _ _. have oT: ordinal_set T. apply:Os_funI => w wc. have ow:= (Os_ordinal oz wc). case: (ozero_dichot ow) => wz. rewrite wz fv ord_induction_y0; exact (proj32 le1). have /lpy le2: inc w (ordinal_interval \1o z). apply /(ointv1 oz); split => //; by apply/(oltP oz). exact: (proj32_1 (ag1 _ _ (oleT ux0 le2) ux0)). have iz1: inc \1o z by apply/(oltP oz). have sT: inc (g (f x \1o) x) T by apply /funI_P; ex_tac. have r1:= (ord_sup_ub oT sT). have ww: x <=o f x \1o by rewrite fv ord_induction_y1; apply: (aw1 _ ux0). exact: (oleT (oleT ww (proj1 (ag1 _ _ (oleT ux0 ww) ux0))) r1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)