nat_pow_add_r@{} n m k : nat_pow n (m + k) = nat_pow n m * nat_pow n k. Proof. induction m as [|m IHm]; simpl. - symmetry. apply nat_add_zero_r. - rhs_V nrapply nat_mul_assoc. exact (ap _ IHm). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids