{A : Type} {x : A} (p : x = x) a b : loopexp p (a + b) = loopexp p a @ loopexp p b. Proof. destruct a as [a| |a], b as [b| |b]; trivial; try apply loopexp_pos_add; cbn. 1,6: symmetry; apply concat_p1. 2,3: symmetry; apply concat_1p. 1: apply loopexp_binint_pos_sub_l. apply loopexp_binint_pos_sub_r. Qed.
Require Import Basics. Require Import Types.Universe. Require Import Spaces.Pos. Require Import Spaces.BinInt.Core. Require Import Spaces.BinInt.Spec. Require Import Spaces.BinInt.Equiv.