mathlib

3348bed9 - chore(tactic/linarith): remove unneeded code (#16791)

chore(tactic/linarith): remove unneeded code (#16791) Removes some unneeded lemmas (and consequently unneeded imports) in `tactic/linarith/lemmas.lean`, in preparation for porting. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>