proposition: Lemma T1T2range1 x: T1T2 x < epsilon0.
proof: Proof. by elim: x => // a Ha n b _ /=; rewrite T2lt_consE /lt_psi /= Ha. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)