chore(topology/algebra/ordered): move squeeze_zero from metric_space

[urkud]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[urkud]

For some reason I don't understand, apply squeeze_zero fails in normed_space/basic while apply @squeeze_zero ℝ (α×α) _ _ _ _ works. Looks like a Lean bug (or a feature I don't understand) to me. Here is the output of #check @squeeze_zero:

squeeze_zero :
  ∀ {α : Type u_5} {β : Type u_6} [_inst_1 : topological_space α] [_inst_2 : partial_order α]
  [t : orderable_topology α] [_inst_3 : has_zero α] {f g : β → α} {b : filter β},
    (∀ (t : β), 0 ≤ f t) → (∀ (t : β), f t ≤ g t) → tendsto g b (𝓝 0) → tendsto f b (𝓝 0)

[urkud]

Asked here: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/apply.20fails.20to.20synthesize.20type.20class.20instance

[urkud]

Closing because apply squeeze_zero doesn't work with the "generalized" version of squeeze_zero.