proposition: Lemma T1limit_plus alpha beta i: (beta o< E0_phi0 alpha)%e0 -> E0limit beta -> E0limit (Omega_term alpha i + beta)%e0.
proof: Proof. intros H H0; assert (alpha <> E0zero). { intro; subst. apply (Limit_not_Zero H0). destruct beta. red in H. simpl in H. apply LT_one in H. subst. now apply E0_eq_intro. } unfold E0limit; rewrite Omega_term_plus; auto. cbn; case_eq (cnf alpha). - intro H2; destruct H1. apply E0_eq_intro. apply H2. - intros alpha0 n beta0 H2. unfold E0limit in H0; destruct (cnf beta); auto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)