proposition: Lemma L_omega_mult_eqn (i : nat) : forall (k : nat), (0 < k)%nat -> L_omega_mult i k = (exp2 i * S k - 1)%nat.
proof: Proof. induction i. - unfold L_omega_mult; simpl; intro; abstract lia. - intros k Hk; simpl; unfold L_omega_mult; simpl. rewrite IHi; unfold L_omega; simpl; auto. repeat rewrite Nat.mul_succ_r; ring_simplify. generalize (exp2_ge_S i); intro; abstract lia. Qed.
imports: hydras(E0 Canon Paths) hydras(MoreLists Iterates Exp2) Coq(Lia Compare_dec)