nat_dist_r@{} n m k : (n + m) * k = n * k + m * k. Proof. lhs nrapply nat_mul_comm. lhs nrapply nat_dist_l. nrapply ap011; nrapply nat_mul_comm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids