proposition: Lemma read_drop : forall (IA:Inhab A) l (s i:int), 0 <= s <= length l -> index (length l - s) i -> (drop s l)[i] = l[s+i].
proof: Proof. Proof using. introv Hs Hi. rew_index in *. lets (l'&Hl&Hl'): drop_spec s l. { math. } rewrite Hl' at 2. rewrite read_app. case_if*. { false. math. } { fequals. math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)