∀ {α : Type u_1} (β : Type u_2) [inst : AddGroup α] [inst_1 : AddMonoid β] [inst_2 : AddAction β α] (H : AddSubgroup α)
  [AddAction.QuotientAction β H] (b : β) (x x_1 : α),
  (QuotientAddGroup.leftRel H) x x_1 → (QuotientAddGroup.leftRel H) (b +ᵥ x) (b +ᵥ x_1)