proposition: Lemma loopexp_add {A : Type} {x : A} (p : x = x) a b : loopexp p (a + b) = loopexp p a @ loopexp p b.
proof: 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_int_pos_sub_l. apply loopexp_int_pos_sub_r. Qed.
imports: Basics Types.Universe Spaces.Pos Spaces.Int.Core Spaces.Int.Spec Spaces.Int.Equiv