proposition: Theorem lt_succ_le : forall a b, a < b -> nf b -> succ a <= b.
proof: Proof. induction a. inversion 1. simpl. auto with T2. generalize IHa3; case a1; case a2. simpl. 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. Focus 2. simpl. intros. 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. inversion 1. subst gamma2. inversion H5. inversion H11. inversion H17. inversion H16. inversion H24. inversion H16. inversion H16. simpl. intros. inversion H. right;constructor 2;auto with T2. right;constructor 3;auto with T2. right;constructor 4. auto. auto. right;constructor 5;auto with T2. right;constructor 6;auto with T2. Focus 2. intros. simpl. 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. auto with T2. auto with T2. apply IHa0;auto with T2. subst b. inversion H0. constructor. auto with T2. apply le_cons_tail;auto with T2. apply IHa0;auto with T2. subst b. inversion H0. constructor. auto with T2. Qed.
imports: EPSILON0 Arith List Omega Compare_dec Relations Wellfounded Max Tools More_nat AccP not_decreasing EPSILON0 More_nat Gamma0_prelude Gamma0_length term rpo