proposition: Lemma index_app_r : forall l l' i, index l' (i - length l) -> i >= length l -> index (l++l') i.
proof: Proof. Proof using. introv. rew_index. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)