∀ {α : Type u_2} {M : Type u_1} [inst : Monoid α] [inst_1 : MulOneClass M] [inst_2 : MulAction α M]
  [inst_3 : IsScalarTower α M M] (c : Con M) (x x_1 : α) (q : Quotient c.toSetoid), (x * x_1) • q = x • x_1 • q