proposition: Lemma H'_Fin : forall i k : nat, H'_ (E0fin i) k = (i+k)%nat.
proof: Proof. Proof with eauto with E0. induction i. - intros; simpl E0fin; simpl; autorewrite with H'_rw E0_rw ... - intros ;simpl; autorewrite with H'_rw E0_rw ... rewrite IHi; abstract lia. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)