speed up some proofs; some changes (#48)

As in the final seminar, I sped up a few proofs, but many are still
quite slow even by replacing all `simp`s by `simp only`s.
Some typeclass inferences are slow and I don't really know how to deal
with them.

In the final theorems, it looked like we were only really considering
the product as a bilinear function, so I did the same for `toDual_{li}`
and fixed a sorry.