proposition: Lemma critical_limit y: OIax1b u w0 g -> critical_ordinal y -> limit_ordinal y.
proof: Proof. move=> ax [pa pc pd]; move: (ax) => [ax1 ax2]. have oy := proj32 pa. case: (ordinal_limA oy) => // h; first by move: pc; rewrite h => /olt0. move:h=> [z oz yv]. move: pc; rewrite yv ; move /oltSleP => le1. move:(oltS oz); rewrite - yv => lt1. move: (pd _ le1 lt1). rewrite yv (ord_induction_p13 fv ax le1 oz) => eq1. have le3: \2o <=o z. apply /oltSleP; rewrite - yv; exact:(olt_leT olt_2omega pa). have le2':=(olt_leT olt_02 le3). move: ((proj33 ax1) _ _ (ord_induction_p41 fv ax1 le1 le2') le1); rewrite eq1. move /oltSleP => l5. case: (oleNgt l5 (ord_induction_p21d ax le1 le3)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)