Over the years, we've amassed an impressive amount of cruft in rt.util. Most of this stuff isn't actually needed anymore for the restructured Prosa. As discussed in Paris, it would be "a good idea" () for "someone" () to split out the old cruft from the actually used utility lemmas/notations/tactics. Well, this is it.
Nothing is lost here; if we need to "revive" and move one of the cut lemmas from rt.util.classic to rt.util, we can still do that later when the need arises.
This MR is on top of !60 (merged) for obvious reasons.
