proposition: Lemma ord_induction_p21d x y: OIax1b u w0 g -> u <=o x -> \2o <=o y -> x <o (f x y).
proof: Proof. move=> ax1b ux y2; move: (ax1b) => [ax1 _]. have ox:=proj32 ux. have lt1:= (ord_induction_p4 fv ax1 ux olt_01). move: (ole_ltT lt1 (proj33 ax1 _ _ (oleT ux lt1) ux)). rewrite -(ord_induction_p13 fv ax1b ux OS1) => h1; apply: (olt_leT h1). move: (proj32_1 h1);rewrite osucc_one => h2. case: (equal_or_not \2o y) => yn2; first by rewrite -yn2; fprops. exact (proj1 (ord_induction_p8 fv ax1 ux (conj y2 yn2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)