proposition: Lemma loopexp_pos_add {A : Type} {x : A} (p : x = x) (a b : Pos) : loopexp_pos p (a + b)%pos = loopexp_pos p a @ loopexp_pos p b.
proof: Proof. revert a b. induction a as [|a aH] using pos_peano_ind; induction b as [|b bH] using pos_peano_ind; trivial. + rewrite pos_add_1_l in *. unfold loopexp_pos. rewrite pos_peano_ind_beta_pos_succ. change (loopexp_pos p (pos_succ b) @ p = p @ loopexp_pos p (pos_succ b)). rewrite bH; cbn. by rewrite concat_pp_p, loopexp_pos_concat. + rewrite pos_add_1_r in *. unfold loopexp_pos. by rewrite pos_peano_ind_beta_pos_succ. + rewrite pos_add_succ_l. unfold loopexp_pos. rewrite 2 pos_peano_ind_beta_pos_succ. change (loopexp_pos p (a + pos_succ b)%pos @ p = (loopexp_pos p a @ p) @ loopexp_pos p (pos_succ b)). by rewrite aH, 2 concat_pp_p, loopexp_pos_concat. Qed.
imports: Basics Types.Universe Spaces.Pos Spaces.Int.Core Spaces.Int.Spec Spaces.Int.Equiv