proposition: Lemma limit_plus_fin_ok : forall alpha, is_limit alpha -> forall n, limit_plus_fin alpha n (alpha + fin n).
proof: Proof. induction alpha. - cbn;constructor 1. - cbn; inversion 1. + intro n1;case n1. * cbn; constructor 2;auto. change (limit_plus_fin zero 0 (fin 0)). constructor 1. * cbn; case_eq (compare [alpha1, alpha2] [zero, zero]). -- intro H7; generalize (compare_Eq H7). injection 1;intros;subst alpha1;subst alpha2. subst alpha;subst beta. case H3;intro;lt_clean. -- intro H7; generalize (compare_Lt H7). inversion 1;intros;try lt_clean. -- cbn; intros; change (limit_plus_fin (gcons alpha1 alpha2 n zero) (S n2) (gcons alpha1 alpha2 n (fin (S n2)))). constructor. auto. constructor. + destruct n1. * cbn; constructor 2. -- eapply is_limit_ab. eexact H. -- generalize H2; generalize (nf_c H5); elim alpha3. intros; change ( limit_plus_fin zero 0 (fin 0));constructor. constructor. eapply is_limit_ab. eexact H10. case (is_limit_cons_inv H9 H10). intros; apply H8. nf_inv. auto. intro;subst t1;change (limit_plus_fin zero 0 (fin 0));constructor. * cbn; case_eq (compare [alpha1, alpha2] [zero, zero]). intro H7;generalize (compare_Eq H7);injection 1;intros. subst alpha1;subst alpha2;subst beta;subst alpha. generalize (is_limit_ab H). destruct 1;lt_clean. intro H7;generalize (compare_Lt H7);intros. inversion H6;lt_clean. intro. replace (gcons zero zero n1 zero) with (fin (S n1)). constructor 2. generalize (compare_Gt H6);intros. inversion_clear H7;auto with T2. lt_clean. lt_clean. apply IHalpha3. auto. auto. 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)