Equational Reasoning in Coq using Tactic Notations

EquationalReasoningTacticNotation.v

Tactic Notation
  "`Begin " constr(lhs) := idtac.

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(lhs) :=
  (stepl lhs by proof).

Tactic Notation
  "≡⟨ " tactic(proof) "⟩" constr(lhs) "`End" :=
  (now stepl lhs by proof).

Require Import Coq.Init.Peano.

Theorem plus_comm :
  forall (m n : nat), m + n = n + m.
Proof.
  intros m n.
  induction n.
  - `Begin
     (m + 0).
    ≡⟨ now rewrite <- plus_n_O ⟩
     (m).
    ≡⟨ reflexivity ⟩
     (0 + m)
    `End.
  - `Begin
     (m + S n).
    ≡⟨ now rewrite plus_n_Sm ⟩
     (S (m + n)).
    ≡⟨ now rewrite IHn ⟩
     (S (n + m)).
    ≡⟨ reflexivity ⟩
     (S n + m)
    `End.
Qed.