proposition: Lemma length_make : forall n v, n >= 0 -> length (make n v) = n.
proof: Proof. Proof using. introv N. unfold make. case_if. math. unfold length. rewrite LibList.length_make. rewrite~ abs_nonneg. Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)