proposition: Lemma loopexp_pos_inv {A : Type} {x : A} (p : x = x) (n : Pos) : loopexp_pos p^ n = (loopexp_pos p n)^.
proof: Proof. revert n. srapply pos_peano_ind; cbn; trivial. unfold loopexp_pos. intros n q. rewrite 2 pos_peano_ind_beta_pos_succ, q. refine ((inv_pp _ _)^ @ _). apply ap. clear q. revert n. srapply pos_peano_ind; cbn; trivial. intros n q. by rewrite pos_peano_ind_beta_pos_succ, concat_p_pp, q. Qed.
imports: Basics Types.Universe Spaces.Pos Spaces.Int.Core Spaces.Int.Spec Spaces.Int.Equiv