proposition: Lemma sup_critical A y: OIax2 u w0 g -> omega0 <=o y -> ordinal_set A -> \osup A = y -> (forall x, inc x A -> u <=o x) -> (forall x, inc x A -> f x y = y) -> critical_ordinal y.
proof: Proof. move=> ax2 ify osA sA uA hA. move: (ax2) =>[ax1 ax0 _ _]; move: (conj ax1 ax0) => ax. move: (OS_sup osA); rewrite sA => oy. case: (emptyset_dichot A) => nea. case: (oleNgt ify). move: sA; rewrite nea setU_0 -[emptyset]/ \0o => <-; exact: olt_0omega. have ly2: \2o <=o y. move: olt_1omega => /oleSltP; rewrite osucc_one => h; exact:(oleT h ify). have ly1:=(oleT (proj1 olt_12) ly2). have xp1: forall x, inc x A -> x <o y. move => x xA; by move:(ord_induction_p21d ax (uA _ xA) ly2);rewrite (hA _ xA). have uy: u <o y. move:nea => [x xA]; exact: (ole_ltT (uA _ xA)(xp1 _ xA)). apply: is_critical_pr => // x ux xy. have ox:=proj32 ux. rewrite - sA in xy;move: (olt_sup osA xy)=> [z zA [zl _]]. by move: (ord_induction_p16 ax2 ux zl (oleR oy)); rewrite (hA _ zA). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)