proposition: Lemma T1T3_lt_epsilon0 x: T1_T3 x < epsilon0.
proof: Proof. by elim x => // a Ha n b Hb /=;rewrite lt_epsilon0 Ha eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)