proposition: Lemma lt_epsilon0 a b c n d : cons a b c n d < epsilon0 = [&& a==zero, b == zero & c < epsilon0 ].
proof: Proof. rewrite psi_lt1 T3lt_psi /lt_psi !T3ltn0 !T3lt0n !T3lt1 /= !andbF !orbF. by case pa: (a== zero) => /=; rewrite ? orbF // T3eqE pa /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)