在Coq中，有几种方法可以避免重复使用代码。

1. 定义可重用的函数或引理：将重复使用的代码封装为一个函数或引理，然后在需要的地方调用它。这样可以避免代码重复，提高代码的可读性和可维护性。

示例代码：

Definition double (n : nat) : nat :=
  n + n.

Lemma double_add_same : forall n, double n = n + n.
Proof.
  intros n.
  unfold double.
  reflexivity.
Qed.

2. 使用参数化的定理：如果重复的代码在一定程度上是相似的，但具有一些差异，可以考虑使用参数化的定理。参数化的定理允许在证明中使用不同的参数值，从而减少代码的重复。

示例代码：

Lemma double_add : forall n m, double (n + m) = double n + double m.
Proof.
  intros n m.
  unfold double.
  rewrite Nat.add_assoc.
  reflexivity.
Qed.

3. 使用Ltac自动化重复的证明步骤：如果重复的证明步骤较为固定，可以使用Coq的Ltac语言来自动化这些步骤。Ltac允许定义自定义的策略，将一组证明步骤封装为一个策略，然后在需要的地方调用它。

示例代码：

Ltac double_rewrite :=
  unfold double;
  rewrite Nat.add_assoc;
  reflexivity.

Lemma double_add_same' : forall n, double n = n + n.
Proof.
  intros n.
  double_rewrite.
Qed.

以上是几种在Coq中避免重复使用代码的解决方法。可以根据具体问题的需要选择适合的方法。