{A : Type} {x : A} (p : x = x) m n : loopexp p (m + n) = loopexp p m @ loopexp p n. Proof. induction m as [|m|m]. - symmetry; apply concat_1p. - rewrite int_add_succ_l. rewrite 2 loopexp_succ_l. by rewrite IHm, concat_p_pp. - rewrite int_add_pred_l. rewrite 2 loopexp_pred_l. by rewrite IHm, concat_p_pp. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.