proposition: Lemma make_succ_l : forall n v, n >= 0 -> make (n+1) v = v :: make n v.
proof: Proof. Proof using. introv N. unfold make. case_if; case_if; try solve [false;math]. rewrite <- LibList.make_succ. fequal. { rewrite succ_abs_eq_abs_one_plus. fequal. math. math. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)