nat_pow_mul_l@{} n m k : nat_pow (n * m) k = nat_pow n k * nat_pow m k. Proof. induction k as [|k IHk]; simpl. 1: reflexivity. lhs_V nrapply nat_mul_assoc. rhs_V nrapply nat_mul_assoc. nrapply ap. rhs nrapply nat_mul_comm. rhs_V nrapply nat_mul_assoc. nrapply ap. rhs nrapply nat_mul_comm. exact IHk. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids