int_dist_r@{} (x y z : Int) : (x + y) * z = x * z + y * z. Proof. by rewrite int_mul_comm, int_dist_l, !(int_mul_comm z). Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.