Simple proofs using Rewrite in Coq, taken from Proof by Rewriting section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html

rewriting.v

(* taken from the Proof by Rewriting section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Theorem plus_id : forall n m : nat,
  n = m -> n + n = m + m.
Proof.
  intros.
  rewrite <- H.
  reflexivity.
Qed.

Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros.
  rewrite -> H.
  rewrite -> H0.
  reflexivity.
Qed.

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros.
  rewrite -> plus_O_n.
  reflexivity.
Qed.

Theorem plus_1_l : forall n:nat,
  1 + n = S n.
Proof.
  intros.
  reflexivity.
Qed.

Theorem mult_S_1 : forall n m : nat,
  m = S n ->
  m * (1 + n) = m * m.
Proof.
  intros.
  rewrite -> plus_1_l.
  rewrite <- H.
  reflexivity.
Qed.

Note, I had to reintroduce the plus_1_l theorem from a different section.