Kstar sub one

@[scoped grind =]theorem kstar_sub_one : l∗ - 1 = (l - 1) * l∗ := by  ext x; constructor  · rintro ⟨h1, h2⟩    obtain ⟨xl, rfl, h_xl⟩ := kstar_def_nonempty l ▸ h1    have h3 : ¬ xl = [] := by grind [one_def]    obtain ⟨x, xl', h_xl'⟩ := exists_cons_of_ne_nil h3    subst h_xl'    refine ⟨x, mem_preimage.mp (h_xl x ?_), xl'.flatten, join_mem_kstar ?_, ?_⟩ <;> grind  · rintro ⟨y, ⟨h_y, h_1⟩, z, h_z, rfl⟩    refine ⟨?_, ?_⟩    · apply (show l * l∗ ≤ l∗ by exact mul_kstar_le_kstar)      exact ⟨y, h_y, z, h_z, rfl⟩    · grind [one_def, append_eq_nil_iff]