proposition: Lemma make_zero : forall v, make 0 v = nil.
proof: Proof. Proof using. intros. unfold make. case_if. { false; math. } asserts_rewrite (abs 0 = 0%nat). { applys eq_nat_of_eq_int. rewrite abs_nonneg; math. } auto. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)