proposition: Lemma make_succ_r : forall n v, n >= 0 -> make (n+1) v = make n v & v.
proof: Proof. Proof using. intros. asserts IA: (Inhab A). applys Inhab_of_val v. applys eq_of_extens_range. { rewrite length_make. rew_list. rewrite length_make. math. math. math. } { intros i Ei. rewrite length_make in Ei; [| math ]. rewrite read_make; [| rewrite int_index_eq; math ]. rewrite read_app. rewrite length_make; [|math]. case_if as C. { rewrite read_make. auto. rewrite int_index_eq; math. } { math_rewrite (i-n = 0). rewrite~ read_zero. } } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)