{A : Type} {x : A} (p : x = x) (z : Int) : loopexp p z.-1 = p^ @ loopexp p z. Proof. rewrite loopexp_pred_r. induction z as [|z|z]. - exact (concat_1p _ @ (concat_p1 _)^). - rewrite loopexp_succ_r. lhs nrapply concat_pp_V. rhs nrapply concat_p_pp. by apply moveL_pM. - rewrite loopexp_pred_r. rhs nrapply concat_p_pp. f_ap. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.