proposition: Lemma T1toB_small x : T1toB x <o epsilon0.
proof: Proof. move: (ord_eps_p3 epsilon0p) => H. elim:x. exact: (olt_ltT olt_0omega H). move => a ha n b hb. apply: (sum_lt_eps0 (prod_lt_eps0 (pow_lt_eps0 ha) (nat_to_B_Nat n.+1)) hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)