coqで2 ^ k + 2 ^ k = 2 ^ (k + 1)の等式でexpnD.を適応したい

Question

coqで2 ^ k + 2 ^ k = 2 ^ (k + 1)の等式でexpnD.を適応したい

expnD
     : forall m n1 n2 : nat, m ^ (n1 + n2) = m ^ n1 * m ^ n2

Lemma expn_twice: forall (k : nat), 2^k + 2^k = 2^(k+1).

左側の2^(k+1)の部分にexpnDを適応したいが出来ない

Answer 1

move=> k.
rewrite expnD.

すると、左辺が　2 ^ k * 2 ^ 1 になりますから、さらに

rewrite expn1 muln2 -addnn.

で書き換えると右辺と同じになります。

すこしまとめると、以下のようになります。

Lemma expn_twice: forall (k : nat), 2^k + 2^k = 2^(k+1).
Proof.
move=> k.
rewrite expnD expn1 muln2 -addnn.
done.
Qed.

以上