proposition: Lemma T1T2range2 x: T2nf x -> x < epsilon0 -> {y: T1 | x = T1T2 y}.
proof: Proof. elim: x => //; first by exists CantorOrdinal.zero. move => a _ b Hb n c Hc /= /and4P [na nb nc nd]. rewrite T2lt_consE /lt_psi !T2ltn0 /= !if_same T2lt1 /= !andbF !orbF if_simpl. move => h; move: h nd => /andP[/eqP -> /(Hb nb)] [y1 ->] hh. have aux:[zero, T1T2 y1] < epsilon0 by rewrite T2lt_psi /lt_psi /= T1T2range1. have [y2 -> ] := (Hc nc (T2lt_trans hh aux)). by exists (CantorOrdinal.cons y1 n y2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)