Introducing linarith

[awalterschulze]

Proof more theorems on lists

This update all started with trying to prove more theorems on lists Introducing the linarith tactic seemed like a good idea This resulted in simplifying quite a few theorems, because simp relies on import magic

more simp only

I use simp? to make theorems more robust for next time we introduce a new import, by copying the output of simp? to replace simp with a simp only ...

Remove imports of already declared types in Mathlib

I had to remove the following imports, since they are important for our project and they cause errors

import Katydid.Std.Algebra
import Katydid.Std.Ordering
import Katydid.Std.ThunkOrdering

These causes errors like:

./././Katydid.lean:1:0: error: import Katydid.Std.Ordering failed, environment already contains 'instReprOrdering._closed_1._cstage2' from Mathlib.Init.Data.Ordering.Basic

and

./././Katydid.lean:1:0: error: import Mathlib.Algebra.Group.Defs failed, environment already contains 'Monoid.toSemigroup' from Katydid.Std.Algebra
error: external command `/Users/walterschulze/.elan/toolchains/leanprover--lean4---nightly-2023-07-12/bin/lean` exited with code 1

Add Algebra Examples

We will delete these at some point, but I'll use them in a presentation soon