Use tactic notations

[Kethku]

I dont know what this means, but it was suggested and everybody nodded, so I assume its good.

[wilcoxjay]

I believe one of the concrete suggestions was something like

Require Import StructTact.StructTactics.

Tactic Notation "find_rewrite" "<-" := find_reverse_rewrite.

Goal forall x y z : nat, x = y -> y = z -> x = z.
Proof.
  intros.
  find_rewrite <-.
  assumption.
Qed.

To make the syntax more similar to rewrite.