proposition: Lemma indecomp_closed_noncoll: iclosed_proper indecomposable.
proof: Proof. move: indecomp_sup => h. have ha: ordinal_prop indecomposable by move => x [/proj32_1 xp _]. split => // [] [E ep]. have ose: ordinal_set E by move => x /ep [/proj32_1 xp _]. move: (OS_sup ose) => os; move: (OS_succ os)=> oy. have yp: \0o <o osucc (union E) by apply: olt0S. move: (indecomp_prod2 yp); set z := _ *o _; move => [sa sb sc]. case: (oltNge (olt_leT (oltS os) (proj1 sb))). by apply:(ord_sup_ub ose); apply/ ep. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)