proposition: Lemma critical_closed_proper: OIax2 u w0 g -> ordinalp u -> iclosed_proper critical_ordinal.
proof: Proof. move => ax2 ou. split. split;first by move => t [/proj32]. by move => F HF neF; apply:sup_critical3. apply: unbounded_non_coll => x ox. have ou2 := OS_sum2 ou OS2. set t := x +o (u +o \2o). case:(sup_critical2 ax2 ou (osum_M0le ox ou2)); set y := \osup _ => qa qb. exists y => //; exact: (oleT (osum_Mle0 ox ou2) qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)