law drop_replicate

bend-mathlib@0.8.1.0 · list.bend:1240

import Base

1240# Dropping m from n copies of x gives n - m copies of x.
1241law drop_replicate:
1242  for -A: Data
1243  for n: Nat
1244  for m: Nat
1245  for -x: A
1246  {List.drop(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.sub(n, m), x) : List<&2, A>}