proposition: Lemma succ_lt_le : forall a b, nf a -> nf b -> a < succ b -> a <= b.
proof: Proof. intros. tricho a b H2; auto with T2. generalize (lt_succ_le H2 H). intro. case (lt_irr (alpha:=succ b)). eapply le_lt_trans;eauto 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