proposition: Lemma lt_epsilon0_succ : forall a, lt_epsilon0 a -> lt_epsilon0 (succ a).
proof: Proof. induction a. - cbn;repeat constructor. - cbn; case a1. + case a2. * repeat constructor. * constructor. -- inversion H;auto with T2. -- apply IHa3. inversion H;auto with T2. + 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)