proposition: Lemma psi_lt_epsilon0 : forall a b, [a, b] t2< epsilon0 -> a = zero /\ b t2< epsilon0.
proof: Proof. intros a b H; inversion H using lt_01. - split. + apply lt_one_inv;auto with T2. + compute;auto with T2. - inversion 1. - inversion 2. - inversion 1. - inversion 1. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)