nat_mul_comm@{} n m : n * m = m * n. Proof. induction m as [|m IHm]; simpl. - nrapply nat_mul_zero_r. - lhs nrapply nat_mul_succ_r. lhs nrapply nat_add_comm. snrapply (ap (nat_add n)). exact IHm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids