proposition: Lemma ord_induction_p9 x y: OIax1 -> u <=o x -> ordinalp y -> y <=o (f x y).
proof: Proof. move=> ax1 ux; move: y; apply: least_ordinal2 => t ot lpy. case: (ozero_dichot ot). move => ->; exact:(ole0x (proj31_1 (ord_induction_p01 ax1 ux))). move => tp. have orf: ordinalp (f x t) by apply: ord_induction_p5. case: (oleT_el ot orf)=> // p3z. case:(oleNgt (lpy _ p3z) (ord_induction_p8 ax1 ux p3z)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)