能否在Coq中重命名项？以double_plus引理归纳步骤为例

我正在学习《Logical Foundations》，已经完成引理double_plus的证明：

Lemma double_plus : forall n, double n = n + n .
Proof.
  induction n.
  - simpl. reflexivity.
  - simpl. rewrite <- plus_n_Sm. rewrite IHn. reflexivity.
Qed.

在归纳步骤中，我的目标是：double (S n) = S n + S n。我想知道是否可以将(S n)设为k，并通过类似如下方式完成证明：

(* double k = k + k *)
rewrite IH. (*k + k = k + k*)
reflexivity.

当然可以通过变量替换的思路简化这一步的证明，不过要注意初始的归纳假设IHn是针对n的，直接替换S n为k后，需要先把归纳假设转换为针对k的形式，以下是两种可行的实现方式：

方式一：用pose定义变量并转换归纳假设 #

Lemma double_plus : forall n, double n = n + n .
Proof.
  induction n.
  - simpl. reflexivity.
  - pose (k := S n). (* 将S n定义为k *)
    replace n with (pred k) by (simpl; reflexivity). (* 把n替换成k的前驱，关联归纳假设 *)
    rewrite IHn. (* 此时归纳假设已适配k相关的目标 *)
    reflexivity.
Qed.

方式二：归纳时直接指定后继变量名（更简洁） #

Lemma double_plus : forall n, double n = n + n .
Proof.
  induction n as [|k]. (* 归纳时将后继步骤的变量直接命名为k *)
  - simpl. reflexivity.
  - simpl.
    (* 此时目标为double (S k) = S k + S k，归纳假设IHk是关于k的：double k = k + k *)
    rewrite <- plus_n_Sm.
    rewrite IHk.
    reflexivity.
Qed.

需要注意的是，你设想的直接rewrite IH无法直接生效，因为初始的归纳假设只对n成立，必须先完成变量的关联转换，才能将归纳假设应用到k=S n的场景中。

内容的提问来源于stack exchange，提问作者udduu