finished the nonassociativenonring stuff (concrete reps are nanrings). it might be a bit messy in places, but it's proven!