∀ {G : Type u_2} {P : Type u_3} {Q : Type u_1} [inst : AddGroup G] [inst_1 : AddTorsor G P] [inst_2 : VAdd G Q]
  [inst_3 : VSub G Q] (f : Q → P) (hf : Function.Injective f) (vadd : ∀ (c : G) (x : Q), f (c +ᵥ x) = c +ᵥ f x),
  (∀ (x y : Q), x -ᵥ y = f x -ᵥ f y) → ∀ (x y : Q), (x -ᵥ y) +ᵥ y = x