feat(linear_algebra/affine_space/combination): vsub distributivity lemmas (#10786)
feat(linear_algebra/affine_space/combination): vsub distributivity lemmas (#10786)

Add lemmas about weighted sums of `-ᵥ` expressions in terms of
`weighted_vsub_of_point`, `weighted_vsub` and `affine_combination`,
with special cases where the points on one side of the subtractions
are constant, and lemmas about those three functions for constant
points used to prove those special cases.

These were suggested by one of the lemmas in #10632; the lemma
`affine_basis.vsub_eq_coord_smul_sum` is a very specific case, but
showed up that these distributivity lemmas were missing (and should
follow immediately from
`sum_smul_const_vsub_eq_vsub_affine_combination` in this PR).







leanprover-community/mathlib,leanprover-community/mathlib