(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
inductive minuss: nat → relation (list2 nat nat) ≝
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
inductive minuss: nat → relation (list2 nat nat) ≝
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
minuss i ({d, e} @ des1) ({d - i, e} @ des2)
| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
minuss i ({d, e} @ des1) ({d - i, e} @ des2)
| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
-fact minuss_inv_nil1_aux: â\88\80des1,des2,i. des1 â\96 i â\89¡ des2 â\86\92 des1 = â\9f â\86\92 des2 = â\9f .
+fact minuss_inv_nil1_aux: â\88\80des1,des2,i. des1 â\96 i â\89¡ des2 â\86\92 des1 = â\97\8a â\86\92 des2 = â\97\8a.
/2 width=4 by minuss_inv_nil1_aux/ qed-.
fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
/2 width=4 by minuss_inv_nil1_aux/ qed-.
fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →