proposition: Lemma limit_plus_F_plus : forall alpha alpha' p, limit_plus_F alpha p alpha' -> nf alpha -> alpha' = alpha + F p.
proof: Proof. induction alpha. inversion_clear 1. simpl;auto. inversion_clear 1. generalize (IHalpha3 gamma p). intros. rewrite (H H1). simpl. case p;simpl. rewrite plus_alpha_0;trivial. caseEq (compare [alpha1, alpha2] [zero, zero]). intro H3; generalize (compare_eq_rw H3). injection 1;intros;subst alpha1;subst alpha2. decompose [or] H0; lt_clean. intro H3; generalize (compare_lt_rw H3). inversion_clear 1;try lt_clean. auto. nf_inv. 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