proposition: Lemma make_eq_cons_make_pred : forall n v, 0 < n -> make n v = v :: (make (n-1) v).
proof: Proof. Proof using. intros. math_rewrite (n = (n-1)+1). rewrite make_succ_l. fequals_rec. math. math. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)