CoordinateProofs.naturals_drop: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as CoordinateProofs
Lines 173-180 of bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&start_line=173&end_line=180

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

def naturals_drop(+values: List<&2, U32>, +count: Nat) -> {Shape.naturals(List.drop(&2, U32, values, count)) == List.drop(&2, Nat, Shape.naturals(values), count) : List<&2, Nat>}:
  match values count:
    case Nil{} count:
      {==}
    case head <> tail 0n:
      {==}
    case head <> tail 1n+rest:
      naturals_drop(tail, rest)

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.drop
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals