proposition: Lemma limit_plus_fin_lim : forall alpha alpha' p, limit_plus_fin 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. * intro H18;rewrite H18;constructor 1;auto. nf_inv. nf_inv. + left; inversion H0; case (H _ _ H9). * nf_inv. * constructor; auto. * intro H10;rewrite H10;constructor;try nf_inv;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)