proposition: Lemma length_drop : forall n l, n <= length l -> length (drop n l) = Z.min (length l) (length l - n).
proof: Proof. Proof using. intros. tests: (0 <= n). { rewrite~ length_drop_nonneg. } { rewrite~ drop_neg. } Qed.
imports: TLC(LibTactics LibLogic LibOperation LibReflect LibProd LibNat LibInt LibOption LibWf) TLC(LibInt)