proposition: Lemma loopexp_int_pos_sub_l {A : Type} {x : A} (p : x = x) (a b : Pos) : loopexp p (int_pos_sub a b) = loopexp_pos p^ b @ loopexp_pos p a.
proof: 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_Vp. + cbn; rewrite int_pos_sub_succ_r. unfold loopexp_pos. rewrite pos_peano_ind_beta_pos_succ. by rewrite concat_pp_p, concat_Vp, concat_p1. + rewrite int_pos_sub_succ_l; cbn. unfold loopexp_pos. rewrite pos_peano_ind_beta_pos_succ. rewrite loopexp_pos_concat. by rewrite concat_p_pp, concat_Vp, concat_1p. + rewrite int_pos_sub_succ_succ. unfold loopexp_pos. rewrite 2 pos_peano_ind_beta_pos_succ. change ((loopexp_pos p^ b @ p^) @ (loopexp_pos p a @ p) = loopexp p (int_pos_sub a b)). rewrite (loopexp_pos_concat p). rewrite concat_pp_p, (concat_p_pp p^ p). rewrite concat_Vp, concat_1p. apply aH. Qed.
imports: Basics Types.Universe Spaces.Pos Spaces.Int.Core Spaces.Int.Spec Spaces.Int.Equiv