proposition: Lemma limit_plus_fin_plus : forall alpha alpha' p, limit_plus_fin alpha p alpha' -> nf alpha -> alpha' = alpha + fin p.
proof: Proof. induction alpha. - inversion_clear 1. cbn;auto. - inversion_clear 1; generalize (IHalpha3 gamma p). intros H H2; rewrite (H H1); cbn. case p;cbn. + rewrite plus_alpha_0;trivial. + case_eq (compare [alpha1, alpha2] [zero, zero]). * intro H3; generalize (compare_Eq H3). injection 1;intros;subst alpha1;subst alpha2. decompose [or] H0; lt_clean. * intro H3; generalize (compare_Lt H3). inversion_clear 1;try lt_clean. * auto. + nf_inv. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)