def len_drop

bend-collections-laws-math@1.0.0.0 · proofs/lib/two_list.bend:26

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

26def len_drop(-T: Data, +xs: List<&2, T>, +k: Nat) -> {SC.length(T, SC.drop(T, xs, k)) == Nat.sub(SC.length(T, xs), k) : Nat}:
27  match xs k:
28    case Nil{} _:
29      Equal.sym(Nat, Nat.sub(0n, k), 0n, zero_sub(k))
30    case Con{h, t} 0n:
31      Equal.sym(Nat, Nat.sub(1n+SC.length(T, t), 0n), 1n+SC.length(T, t), N.sub_zero(1n+SC.length(T, t)))
32    case Con{h, t} 1n+p:
33      len_drop(T, t, p)