proposition: Lemma P_alpha_0 : P alpha.
proof: Proof. destruct (Zero_Limit_Succ_dec alpha). destruct s. - subst; apply PZero. - split. apply RAlim; auto. intro; apply RBlim; auto. apply RClim; auto. apply RDlim; auto. apply RElim; auto. - destruct s; split. eapply PA_Succ;eauto. eapply RB;eauto. eapply RC;eauto. eapply RD;eauto. eapply RE;eauto. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)