proposition: Lemma indecomp_sup E: (forall x, inc x E -> indecomposable x) -> (nonempty E) -> indecomposable (\osup E).
proof: Proof. move => ai [w wE]. have osE: ordinal_set E by move => t /ai [/proj32_1 h _]. move: (ord_sup_ub osE wE); set x := \osup E => wx. have xp:= (olt_leT (proj1 (ai _ wE)) wx). split=> // a b /(olt_sup osE)[a' a'E aa'] /(olt_sup osE) [b' b'E bb']. move:(omax_p1 (proj32_1 aa') (proj32_1 bb'));set z := omax a' b'. move => [za zb]. have zE: inc z E by apply: Gmax_E. have az := olt_leT aa' za. have bz := olt_leT bb' zb. move => abx; move: (ord_sup_ub osE zE); rewrite -/x -abx => l1. case: (oleNgt l1 (indecomp_prop2 az bz (ai _ zE))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)