proposition: Lemma length_take : forall n l, n <= length l -> length (take n l) = Z.max 0 n.
proof: Proof. Proof using. intros. tests: (0 <= n). { rewrite~ length_take_nonneg. } { rewrite~ take_neg. rewrite~ Z.max_l. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)