proposition: Lemma indecomp_sup1 x: \0o <o x -> exists y, [/\ indecomposable y, y <=o x & forall z, indecomposable z -> z <=o x -> z <=o y].
proof: Proof. move=> xp. have ox:=proj32_1 xp. set E := Zo (osucc x) indecomposable. have pa: (forall t, inc t E -> indecomposable t) by move =>t /Zo_P [_]. have pb: nonempty E. exists \1o; apply:Zo_i; last by apply:indecomp_one. move /oltSSP: xp => /(oltP (OS_succ ox)). by rewrite osucc_zero. have pc: (forall t, inc t E -> t <=o x) by move =>t /Zo_P [] /(oleP ox). have osE: ordinal_set E by move => t /pc []. move: (ord_sup_ub osE)(OS_sup osE) (ord_ub_sup ox pc) => pe pf pg. move: (indecomp_sup pa pb) => h; exists (\osup E); split => // z za zx. by apply: pe; apply: Zo_i =>//; apply /(oleP ox). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)