intro j k h
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
⊢ Function.Injective (tw n d)
n✝ d✝ : ℕ
inst✝¹ : NeZero d✝
n d : ℕ
inst✝ : NeZero d
j k : Fin (Nat.succ n)
h : tw n d j = tw n d k
⊢ j = k