proposition: Lemma ord_induction_p5 x y: OIax1 -> u <=o x -> ordinalp y -> ordinalp (f x y).
proof: Proof. move=> ax1 ux oy; case: (ozero_dichot oy) => y1. by move: (ord_induction_p01 ax1 ux); rewrite y1; move => [[]]. exact: (proj32 (ord_induction_p4 ax1 ux y1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)