proposition: Lemma T2toB_small x : T2toB x <o Gamma_0.
proof: Proof. elim:x. rewrite /= - Gamma0_epsilon; apply:(oopow_pos OS_Gamma_0). by move => a ha b hb n c hc; apply:T2_to_bourbaki_small. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)