proposition: Lemma take_pos_last : forall (IA:Inhab A) l i, index l (i-1) -> take i l = take (i-1) l & l[i-1].
proof: Proof. Proof using. introv Hi. gen i. induction l; intros; rew_index in Hi; rew_list in Hi. { math. } { rewrite take_cons_pos; try math. rewrite take_cons_case; try math. case_if as C. { rew_list. rewrite C. rewrite take_zero. rewrite* read_zero. } { rew_list. fequals. rewrite IHl; [|rew_index;math]. fequals. rewrite* read_cons_pos. math. } } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)