proposition: Lemma iclosed_ord x: ordinalp x -> iclosed_set x.
proof: Proof. move => ox. have osx:= Os_ordinal ox. split => // F fo _. have h:= (ord_ub_sup1 ox fo). case:(ole_eqVlt h) => e1; last by right;apply /(oltP ox). left; apply: (ord_sup_1cofinal _ osx); split => // a ax. have au: a <o union F by rewrite e1; apply /oltP. move:(@olt_sup F a (Os_sub osx fo) au)=> [z za [zb _]]; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)