{A : Type} {x : A} (p : x = x) (a b : Pos) : loopexp p (binint_pos_sub a b) = loopexp_pos p a @ loopexp_pos p^ b. Proof. symmetry. revert a b. induction a as [|a aH] using pos_peano_ind; induction b as [|b bH] using pos_peano_ind. + apply concat_pV. + cbn; rewrite binint_pos_sub_succ_r. unfold loopexp_pos. rewrite pos_peano_ind_beta_pos_succ. change (p @ (loopexp_pos p^ b @ p^) = loopexp p (neg b)). rewrite loopexp_pos_concat. by rewrite concat_p_pp, concat_pV, concat_1p. + rewrite binint_pos_sub_succ_l; cbn. unfold loopexp_pos. rewrite pos_peano_ind_beta_pos_succ. change ((loopexp_pos p a @ p) @ p^ = loopexp_pos p a). by rewrite concat_pp_p, concat_pV, concat_p1. + rewrite binint_pos_sub_succ_succ. unfold loopexp_pos. rewrite 2 pos_peano_ind_beta_pos_succ. change ((loopexp_pos p a @ p) @ (loopexp_pos p^ b @ p^) = loopexp p (binint_pos_sub a b)). rewrite (loopexp_pos_concat p^). rewrite concat_pp_p, (concat_p_pp p p^). rewrite concat_pV, concat_1p. apply aH. 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.