coq - Coq で方程式の両辺に群要素を掛ける Ltac の書き方

Question

このグループの定義を使用すると、次のようになります。

Structure group :=
  {
    G :> Set;

    id : G;
    op : G -> G -> G;
    inv : G -> G;

    op_assoc_def : forall (x y z : G), op x (op y z) = op (op x y) z;
    op_inv_l : forall (x : G), id = op (inv x) x;
    op_id_l : forall (x : G), x = op id x
  }.

(** Set implicit arguments *)
Arguments id {g}.
Arguments op {g} _ _.
Arguments inv {g} _.

Notation "x # y" := (op x y) (at level 50, left associativity).

そして、この定理を証明すると:

Theorem mult_both_sides (G : group) : forall (a b c : G),
    a = b <-> c # a = c # b.

与えられた等式 (目標自体または仮説) に与えられた項を乗算するプロセスを自動化する Ltac をどのように記述すればよいでしょうか?

理想的には、証明でこの Ltac を使用すると、次のようになります。

left_mult (arbitrary expression).
left_mult (arbitrary expression) in (hypothesis).