proposition: Lemma PZero : P E0zero.
proof: Proof. split; auto with T1; ord_eq (E0_succ E0zero) (E0fin 1). all: try (rewrite H;auto with T1). unfold Canon_plus; intros beta n H0; unfold E0zero in H0; simpl in H0. destruct n. - inversion H0. - destruct (const_pathS_zero H0). Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)