nat_mul_assoc@{} n m k : n * (m * k) = n * m * k. Proof. induction n as [|n IHn]; simpl. - reflexivity. - rhs nrapply nat_dist_r. nrapply (ap (nat_add (m * k))). exact IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids