∀ {α : Type u_2} {β : Type u_1} [inst : KleeneAlgebra α] [inst_1 : LE β] [inst_2 : LT β] [inst_3 : Zero β]
  [inst_4 : One β] [inst_5 : Add β] [inst_6 : Mul β] [inst_7 : Pow β ℕ] [inst_8 : SMul ℕ β] [inst_9 : NatCast β]
  [inst_10 : Max β] [inst_11 : Bot β] [inst_12 : KStar β] (f : β → α) (hf : Function.Injective f)
  (le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : β}, f x < f y ↔ x < y) (zero : f 0 = 0) (one : f 1 = 1)
  (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = f x * f y)
  (nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n)
  (natCast : ∀ (n : ℕ), f ↑n = ↑n) (sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) (bot : f ⊥ = ⊥),
  (∀ (a : β), f (KStar.kstar a) = KStar.kstar (f a)) → ∀ (a b : β), a * b ≤ b → KStar.kstar a * b ≤ b