proposition: Lemma LF1 : forall i, F_ 1 i = S (2 * i).
proof: Proof. intro i; unfold E0fin; rewrite FinS_Succ_eq, F_succ_eqn. rewrite iterate_rw, F_zero_eqn. simpl; rewrite iterate_ext with (g := S). - undiag2 i 1 3. + simpl; abstract lia. + simpl; auto. - intro; now rewrite F_zero_eqn. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)