proposition: Lemma is_critical_pr y: OIax1b u w0 g -> omega0 <=o y -> u <o y -> (forall x, u <=o x -> x <o y -> f x y <=o y) -> critical_ordinal y.
proof: Proof. move=> ax p1 p2 p3; split => // x ux xy; apply: (oleA (p3 _ ux xy)). have oy:= proj32 p1. exact:(oleT (osum_M0le (proj32 ux) oy) (ord_induction_p21c ax ux p1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)