proposition: Lemma ord_induction_p7 x y y': OIax1 -> u <=o x -> y <o y' -> g (f x y) x <=o (f x y').
proof: Proof. move=> ax1 ux yz. have [[oy oy' _] _] := yz. have yp:= (ole_ltT (ole0x oy) yz). rewrite fv (ord_induction_yp w0 g x yp) -fv. rewrite /ord_induction_sup;set T:= fun_image _ _. have oT: ordinal_set T. by move => z /funI_P [v /(Os_ordinal oy') vz ->]; apply: ord_induction_p6. have iyy:inc y y' by apply/(oltP oy'). apply: (ord_sup_ub oT); apply /funI_P;ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)