proposition: Lemma ord_induction_p8 x y y': OIax1 -> u <=o x -> y <o y' -> (f x y) <o (f x y').
proof: Proof. move=> ax1 ux yz. wlog: y yz / \0o <o y => yp. case: (ozero_dichot (proj31_1 yz)) => y1; last by apply: yp. move: (ord_induction_p01 ax1 ux) => cp. case: (oone_dichot yz)=> y'1; first by rewrite y1 y'1; apply: cp. by move: (ole_ltT (proj1 cp) (yp _ y'1 olt_01)); rewrite y1. have le1:= (ord_induction_p7 ax1 ux yz). have le2:= (ord_induction_p41 ax1 ux yp). exact: (olt_leT (proj33 ax1 _ _ le2 ux) le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)