proposition: Lemma L_ge_S alpha : alpha <> E0zero -> S <<= L_ alpha.
proof: Proof. Proof with auto with E0. pattern alpha; apply well_founded_induction with E0lt ... clear alpha; intros alpha IHalpha. destruct (Zero_Limit_Succ_dec alpha). - destruct s. + intro; contradiction. + intros H k; rewrite L_lim_eqn; auto. * specialize (IHalpha (Canon alpha k)). destruct k; simpl Canon. apply L_ge_id. apply L_ge_id. - destruct s as [beta e]; destruct (E0_eq_dec beta E0zero). + subst beta alpha. intros H k; autorewrite with L_rw; auto. + subst alpha; intros H k; autorewrite with L_rw ... transitivity (S (S k)); [lia |] ... apply IHalpha ... Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)