proposition: Lemma update_cons_pos : forall n v x l, n > 0 -> (x::l)[n:=v] = x::(l[(n-1):=v]).
proof: Proof. Proof using. introv N. unfold update, update_inst, update_impl. do 2 (case_if; try solve [ false; math ]). rewrite~ update_cons_pos. { fequals_rec. rewrite <- abs_gt_minus_nat. fequals. math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)