nat_pow_one_l@{} n : nat_pow 1 n = 1. Proof. induction n as [|n IHn]; simpl. 1: reflexivity. lhs nrapply nat_add_zero_r. exact IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids