fact: Definition rng_plus_assoc : x + (y + z) = (x + y) + z := simple_associativity x y z.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse