proposition: Lemma is_limit_ab : forall alpha beta n gamma, is_limit (cons alpha beta n gamma) -> zero < alpha \/ zero < beta.
proof: Proof. inversion 1. auto. generalize H5 H2 ;case gamma. inversion 2. inversion_clear 1. inversion_clear H7. left;apply le_lt_trans with t;auto with T2. right; apply le_lt_trans with t0;auto with T2. right; apply le_lt_trans with [t,t0];auto with T2. right;apply le_lt_trans with t;auto with T2. lt_clean. lt_clean. 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