proposition: Lemma L_ge_id alpha : forall i, i <= L_ alpha i.
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. + subst alpha. intro; rewrite L_zero_eqn. auto with arith. + intros k; rewrite L_lim_eqn; auto. * specialize (IHalpha (Canon alpha k)). destruct k; simpl Canon. -- autorewrite with L_rw; auto. auto with arith. -- transitivity (S (S k)); [lia | apply IHalpha ]... - destruct s as [beta e]; destruct (E0_eq_dec beta E0zero). + subst beta alpha. intros k; autorewrite with L_rw; auto. + subst alpha; intros k; autorewrite with L_rw ... transitivity (S k); [lia |] ... Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)