proposition: Lemma ord_induction_p17 x x' y: OIax2 u w0 g -> (forall a b b', u <=o a -> u <=o b -> b <o b' -> g a b <o g a b') -> u <=o x -> x <o x' -> ordinalp y -> f x (osucc y) <o f x' (osucc y).
proof: Proof. move=> ax2 gsi ux xx' oy. have lexx':= (proj1 xx'). have lexx:= (oleR (proj32 ux)). have ux':= (oleT ux lexx'). have lt1:= (ord_induction_p16 ax2 ux lexx' (oleR oy)). move: (ax2) => [ax1 ag2 aw2w aw2]. case: (equal_or_not y \0o) => yz. rewrite yz osucc_zero. rewrite fv ! ord_induction_y1; apply: aw2=> //. have y1:= (ord_ne0_pos oy yz). have h3:= (ord_induction_p41 fv ax1 ux y1). have le2: (g (f x y) x) <=o (g (f x' y) x) by apply: ag2. have lt3:(g (f x' y) x) <o (g (f x' y) x') by apply :gsi (oleT h3 lt1) ux xx'. have le4:= (ole_ltT le2 lt3). rewrite (ord_induction_p13 fv (conj ax1 ag2) ux oy). by rewrite (ord_induction_p13 fv (conj ax1 ag2) ux' oy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)