proposition: Lemma map_make : forall A B (f:A->B) (n:int) (v:A), n >= 0 -> map f (make n v) = make n (f v).
proof: Proof. Proof using. Transparent make. intros. unfold make. case_if. { false; math. } applys map_make. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)