law take_replicate

bend-mathlib@0.8.1.0 · list.bend:1221

import Base

1221# Taking m from n copies of x gives min(m, n) copies of x.
1222law take_replicate:
1223  for -A: Data
1224  for n: Nat
1225  for m: Nat
1226  for -x: A
1227  {List.take(&2, A, List.replicate(A, n, x), m) == List.replicate(A, Nat.min(m, n), x) : List<&2, A>}