nat_add_assoc@{} n m k : n + (m + k) = (n + m) + k. Proof. induction n as [|n IHn]. - reflexivity. - nrapply (ap nat_succ). exact IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids