nat_add_comm@{} n m : n + m = m + n. Proof. induction n. - exact (nat_add_zero_r m)^. - rhs nrapply nat_add_succ_r. apply (ap nat_succ). exact IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids