mathlib3

38796213 - feat(combinatorics/additive/salem_spencer): The sphere does not contain arithmetic progressions (#13259)

feat(combinatorics/additive/salem_spencer): The sphere does not contain arithmetic progressions (#13259) Prove that the frontier of a strictly convex closed set is Salem-Spencer. For this we need * simple lemmas about `same_ray`. This involves renaming `same_ray.exists_right_eq_smul`/`same_ray.exists_left_eq_smul` to `same_ray.exists_nonneg_left`/`same_ray.exists_nonneg_right`. * that the norm in a real normed space is injective on rays. * that the midpoint of two points of equal norm has smaller norm, in a strictly convex space