proposition: Lemma id_le_f_alpha (alpha: E0) : forall i, i <= f_ alpha i.
proof: Proof. pattern alpha; apply (well_founded_induction E0lt_wf); clear alpha; intros alpha IHalpha. destruct (Zero_Limit_Succ_dec alpha) as [[HZero | Hlim] | Hsucc]. - subst; intros i ; rewrite !f_zero_eqn; auto with arith. - intros i. rewrite !(f_lim_eqn alpha). + apply IHalpha, Canon_lt; now apply Limit_not_Zero. + apply Hlim. - destruct Hsucc as [beta Hbeta]; subst; intro i; rewrite f_succ_eqn. generalize i at 1 3; induction i. + intros; cbn; auto with arith. + intros; cbn; transitivity (iterate (f_ beta) i i0); auto. apply (IHalpha beta (Lt_Succ beta)). Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)