proposition: Lemma is_limit_intro : forall b1 b2 n , nf b1 -> nf b2 -> zero < b1 \/ zero < b2 -> is_limit (cons b1 b2 n zero).
proof: Proof. constructor;auto. 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