proposition: Theorem H'_L_ alpha : forall i:nat, (H'_ alpha i <= L_ alpha (S i))%nat.
proof: Proof. Proof with auto with E0. pattern alpha ; apply well_founded_induction with E0lt ... clear alpha; intros alpha IHalpha i. destruct (Zero_Limit_Succ_dec alpha) as [[H | H] | H]. - subst; rewrite H'_eq1, L_zero_eqn. abstract lia. - rewrite H'_eq3, L_lim_eqn ... apply Nat.lt_le_incl; apply Nat.lt_le_trans with (H'_ (Canon alpha (S i)) (S i)). apply H'_alpha_mono; auto with arith ... apply IHalpha ... - destruct H as [beta e]; subst alpha; rewrite H'_eq2, L_succ_eqn ... Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)