proposition: Lemma limit_plus_F_lim : forall alpha alpha' p, limit_plus_F alpha p alpha' -> nf alpha -> is_limit alpha \/ alpha=zero.
proof: Proof. intro alpha;elim alpha. auto. intros alpha1 _ alpha2 _ alpha3; case alpha3. left. inversion H0. case (H _ _ H9). nf_inv. constructor. auto. auto. intro H18;rewrite H18;constructor 1;auto. nf_inv. nf_inv. left. inversion H0. case (H _ _ H9). nf_inv. constructor. auto. auto. intro H10;rewrite H10;constructor;try nf_inv. 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