proposition: Lemma sup_Oalpha_succ x: T1nf x -> sup id (T1succ x) x.
proof: Proof. move => nx;split. - done. - by move => y nf; rewrite lt_succ_le_3. - by move => z nz zx; exists x => //; rewrite nx zx succ_lt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)