proposition: Theorem lt_succ_le alpha : forall beta, alpha t2< beta -> nf beta -> succ alpha t2<= beta.
proof: Proof. induction alpha. - inversion 1; cbn; auto with T2. - generalize IHalpha3; case alpha1; case alpha2. + cbn; inversion 2. * right; constructor 2. -- auto with T2. -- auto with T2. * right;constructor 3;auto with T2. * lt_clean. * lt_clean. * inversion H5. case gamma2. -- left;auto with T2. -- right;auto with T2. -- right;constructor 6. auto with arith T2. * inversion 1. -- subst gamma2; inversion H5. -- inversion H11. inversion H17. inversion H16. inversion H24. inversion H16. inversion H16. + cbn; intros t t0 n0 t1 IHa0 b H H0; inversion H. * right;constructor 2;auto with T2. * right;constructor 3;auto with T2. * inversion H5. inversion H5. inversion H6. * inversion H6. * inversion H6. right;constructor 6. auto with arith T2. right;constructor 6. auto with arith T2. * apply le_cons_tail. apply IHa0; auto. subst b; inversion H0;auto with T2. + cbn; intros; inversion H; auto. * right;constructor 2;auto with T2. * right;constructor 3;auto with T2. * right;constructor 4; auto. * right;constructor 5;auto with T2. * right;constructor 6;auto with T2. * apply le_cons_tail;auto with T2. apply IHalpha0;auto with T2. subst ; inversion H0. constructor. auto with T2. + intros; cbn ; inversion H. * right;constructor 2;auto with T2. * right;constructor 3;auto with T2. * right;constructor 4;auto with T2. * right;constructor 5;auto with T2. * right; constructor 6;auto with T2. * apply le_cons_tail;auto with T2. -- apply IHalpha0;auto with T2. ++ subst ; inversion H0; auto with T2. 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)