proposition: Lemma sup_Oalpha_limit x: T1nf x -> T1limit x -> sup id x x.
proof: Proof. move => nx lx ;split; [done | by move => y _ /T1ltW | ]. move => z nz zx; move: (limit_pr lx zx) => h. by exists (T1succ z); rewrite h nf_succ // (succ_lt z). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)