proposition: Lemma H'_alpha_ge_id : id <<= H'_ alpha.
proof: Proof. destruct (E0_eq_dec alpha E0zero). - subst alpha; intro k; rewrite H'_eq1; cbn;auto with arith. - intro k;unfold id; now apply Nat.lt_le_incl, H'_alpha_gt. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)