add class ring_div; generalize mod/diff/minus proofs for class ring_div
By chapter:chapters 1 and 2, maybe 3: Peter Whitechapters 6, 7 and 8: David von Oheimchapter 6, maybe 8: Gerwin Kleinchapters 3, maybe 4: Tanja Voschapters 1-3 at least: Stefano Bistarelli