Tvs 20260304

[affeldt-aist]

Motivation for this change

fyi: @mkerjean

This PR moves the file tvs.v into normedtype_theory in such a way that it only depends num_normedtype.v
and pseudometric_normed_Zmodule (instead of the whole directory).

In the process:

• some structures (that are actually joins) needed to be moved out of tvs.v and
  placed earlier in the file hierarchy (it looks like a good change)
• some local lemmas were turned into Let's (this was an oversight)
• two longish proofs could be shortened (standard_{add,scale}_continuous)
• comments that were suggesting proof sharing have been updated

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[mkerjean]

Simplifying code and allowing for further simpler proofs in tvs.v