coqtokyo_question_0927.v

From mathcomp Require Import ssreflect ssrnat div.


Lemma test_000: forall a b c : nat, a + b + c = b + c + a.
Proof.
  move=> a b c.
  rewrite (_: b + c = c + b).
  - by apply addnCAC.
  - by apply addnC.
Qed.

Lemma test_001: forall m : nat, 2 ^ m.+1 = 2 * 2 ^ m.
Proof.
  move=> m. by rewrite expnS.
Qed.

Lemma test_002: forall a b c : nat, a * b ^ c = b ^ c * a.
Proof.
  move=> a b c. by apply /mulnC.
Qed.

Lemma test_003: forall a b c : nat, a * b ^ c %/ a = b ^ c * a %/ a.
Proof.
  move=> a b c. by rewrite mulnC.
Qed.

Lemma test_004: forall a b c : nat, a + b ^ c = b ^ c + a.
Proof.
  move=> a b c. by rewrite addnC.
Qed.