proposition: Lemma L_finite : forall i k :nat, L_ i k = (i+k)%nat.
proof: Proof. induction i. - simpl E0fin; intro; now rewrite L_zero_eqn. - simpl; rewrite FinS_Succ_eq; intro k; autorewrite with E0_rw L_rw. rewrite IHi. + abstract lia. Qed.
imports: hydras(Hprime E0 Canon Paths Large_Sets) hydras(Simple_LexProd Iterates ) Coq(ArithRing Lia) Equations(Equations)