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