(**************************************************************************)
include "ground/notation/relations/rat_3.ma".
(**************************************************************************)
include "ground/notation/relations/rat_3.ma".
include "ground/relocation/mr2.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
include "ground/relocation/mr2.ma".
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
qed-.
lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @❪i1, ❨l, m❩;cs❫ ≘ i2 →
l ≤ i1 → @❪i1 + m, cs❫ ≘ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
qed-.
lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @❪i1, ❨l, m❩;cs❫ ≘ i2 →
l ≤ i1 → @❪i1 + m, cs❫ ≘ i2.
#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1