{A : Ring} (x y z : A) : (x - y) * z = x * z - y * z. Proof. lhs nrapply rng_dist_r. nrapply ap. nrapply rng_mult_negate_l. Defined.
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.