proposition: Lemma critical_indecomposable y: OIax2 u w0 g -> critical_ordinal y -> indecomposable y.
proof: Proof. move => ax; move: (ax) => [ax1 ax0 _ _]; move: (conj ax1 ax0) => ax1b. move=> [y1 y3 y4]. have oy := proj32 y1. have yp:= (ole_ltT (ole0x (proj31_1 y3)) y3). apply/(indecompP yp) => x xy. move: (proj31_1 xy) (proj31_1 y3) => ox ou. apply: oleA; last exact: (osum_M0le ox oy). have pa: forall t, u <=o t -> t +o y <=o (f t y). by move => t tp; apply: ord_induction_p21c. case: (oleT_ee ox ou) => lexu. have leuu:= (oleR ou). rewrite - {2} (y4 _ leuu y3); apply: oleT (pa _ leuu). by apply: osum_Mleeq. by rewrite - {2} (y4 _ lexu xy); apply: pa. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)