chore(algebra/tropical/basic): remove 3 instances (#11920)
The three removed instances are
* `covariant_swap_add` (exists since addition is commutative and the non-swapped version is proved);
* `covariant_add_lt` (as is, this is a copy of `covariant_add` -- judging from the name, it could have been intended to have a `(<)`, but with `(<)` it is false, see below);
* `covariant_swap_add_lt` (exists since addition is commutative and the non-swapped version is proved).
Here is a proof that the second instance with `(<)` is false:
```lean
lemma not_cov_lt : ¬ covariant_class (tropical ℕ) (tropical ℕ) (+) (<) :=
begin
refine λ h, (lt_irrefl (trop 0) _),
cases h,
have : trop 0 < trop 1 := show 0 < 1, from zero_lt_one,
calc trop 0 = trop 0 + trop 0 : (trop 0).add_self.symm
... < trop 0 + trop 1 : h _ this
... = trop 0 : add_eq_left this.le,
end
```
