proposition: Lemma omega_tower_unbounded x: ~ (forall n, (omega_tower n) < x).
proof: Proof. elim :x; first by move => h; move: (h 0); rewrite T1ltn0. move => a Ha n b _ c; case Ha => m. move: (c m.+2); move /T1lt_cons_le;apply: T1lt_le_trans;apply: head_lt_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)