title: How to write an Ltac to multiply both sides of a equation by a group element in Coq
body: <p>Using this definition of a group:</p>
  
  <pre><code>Structure group :=
    {
      G :&gt; Set;
  
      id : G;
      op : G -&gt; G -&gt; G;
      inv : G -&gt; 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).
  </code></pre>
  
  <p>And having proven this theorem:</p>
  
  <pre><code>Theorem mult_both_sides (G : group) : forall (a b c : G),
      a = b &lt;-&gt; c # a = c # b.
  </code></pre>
  
  <p>How do I write an Ltac that automates the process of left multiplying a given equality (either the goal itself or a hypothesis) by a given term?</p>
  
  <p>Ideally, using this Ltac in a proof would look like this:</p>
  
  <pre><code>left_mult (arbitrary expression).
  left_mult (arbitrary expression) in (hypothesis).
  </code></pre>