law drop_append_of_le_length

bend-mathlib@0.8.1.0 · list.bend:1163

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

1163# Dropping at most the length of the first part of an append drops only from the first part.
1164law drop_append_of_le_length:
1165  for -a: Quant
1166  for -A: Kind(a)
1167  for xs: List<a, A>
1168  for ys: List<a, A>
1169  for n: Nat
1170  for h: MNat.le(n, List.length(a, A, xs))
1171  {List.drop(a, A, List.append(a, A, xs, ys), n) == List.append(a, A, List.drop(a, A, xs, n), ys) : List<a, A>}