proposition: Lemma ord_induction_p16 x y x' y': OIax2 u w0 g -> u <=o x -> x <=o x' -> y <=o y' -> f x y <=o f x' y'.
proof: Proof. move=> [ax1 ag2 aw2w aw2] ux xx' yy'. have ux':= oleT ux xx'. have oy:= proj31 yy'. apply: (@oleT (f x' y)); last first. apply: (sincr_incr _ yy')=> z z'; apply:(ord_induction_p8 fv ax1 ux'). apply:(least_ordinal2 (p:= fun y=> (f x y) <=o (f x' y))) oy => t ot lpy. case: (ozero_dichot ot) => tp. by rewrite tp fv ord_induction_y0 ord_induction_y0; apply:aw2w. rewrite fv (ord_induction_yp w0 g _ tp)(ord_induction_yp w0 g _ tp). rewrite /ord_induction_sup. set T1:= fun_image _ _; set T2:= fun_image _ _. have oT1: ordinal_set T1. move=> v => /funI_P [w /(Os_ordinal ot) ow ->]. rewrite - fv;apply:(ord_induction_p6 fv ax1 ux ow). have oT2: ordinal_set T2. move=> v => /funI_P [w /(Os_ordinal ot) ow ->]. rewrite - fv;apply:(ord_induction_p6 fv ax1 ux' ow). have osT2:= (OS_sup oT2). apply: (ord_ub_sup osT2). move=> i => /funI_P [z /(oltP ot) zt ->]; rewrite - fv. have z2:= (olt_i zt). have oz:= proj31_1 zt. move: (lpy _ zt) => h1. set j :=g (f x' z) x'. have jT2: inc j T2 by apply /funI_P ;exists z => //; rewrite - fv. apply:(oleT _ (ord_sup_ub oT2 jT2)). case: (equal_or_not x x') => exx'. by rewrite /j - exx'; apply:oleR; apply: (ord_induction_p6 fv ax1 ux). case: (ozero_dichot oz) => zz. rewrite /j zz fv ! ord_induction_y0; exact(proj1(aw2 _ _ ux (conj xx' exx'))). by apply: ag2=> //; apply: (ord_induction_p41 fv ax1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)