proposition: Lemma sup_Oalpha_limit x: T3nf x -> T3limit x -> sup_of id x x.
proof: Proof. move => nx lx ;split; [done | by move => y _ /T3ltW | ]. move => z nz H. by exists (T3succ z); rewrite (limit_pr lx H) succ_lt nf_succ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)