nat_pow_mul_r@{} n m k : nat_pow n (m * k) = nat_pow (nat_pow n m) k. Proof. induction m as [|m IHm]; simpl. - exact (nat_pow_one_l _)^. - lhs nrapply nat_pow_add_r. rhs nrapply nat_pow_mul_l. nrapply ap. exact IHm. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids