law drop_replicate_sym

bend-mathlib@0.8.1.0 · list.bend:2658

import Base

2658# Dropping m from n copies of x gives n - m copies of x, reversed to rewrite toward the simple side.
2659law drop_replicate_sym:
2660  for -A: Data
2661  for n: Nat
2662  for m: Nat
2663  for -x: A
2664  {List.replicate(A, Nat.sub(n, m), x) == List.drop(&2, A, List.replicate(A, n, x), m) : List<&2, A>}