proposition: Lemma H'_Plus_Fin alpha : forall i k : nat, H'_ (alpha + i)%e0 k = H'_ alpha (i + k)%nat.
proof: Proof. induction i. - intro k; ochange (alpha + 0)%e0 alpha. + now simpl. + rewrite Plus_rw; simpl; auto with T1. now rewrite plus_zero_r. - intro k; ochange (alpha + (S i))%e0 (E0_succ (alpha + i))%e0. + rewrite H'_eq2, IHi; f_equal; abstract lia. + repeat rewrite Plus_rw; simpl. destruct i; simpl. * rewrite plus_zero_r; now rewrite succ_is_plus_one. * simpl; replace (FS i) with (\F (S i)). -- rewrite succ_of_plus_finite. ++ f_equal. ++ apply cnf_ok. -- reflexivity. Qed.
imports: Coq(ArithRing Lia) hydras(E0 Canon Paths) hydras(Exp2 Iterates Simple_LexProd) hydras(Compat815) Equations(Equations)