proposition: Lemma ord_induction_p11 x b y y': OIax1 -> u <=o x -> ordinalp y -> ordinalp y' -> (f x y) <=o b -> b <o (f x (osucc y)) -> (f x y') <=o b -> b <o (f x (osucc y')) -> y = y'.
proof: Proof. move=> ax1 ux. have h: sincr_ofs (f x) by move => t t';apply:(ord_induction_p8 ax1 ux). apply: (sincr_bounded_unique h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)