def subtract_shift

stelliferous@0.0.2.0 · proofs/nat_order.bend:40

import Base

40def subtract_shift(+first: Nat,+row: Nat) -> {Nat.sub(Nat.add(first,row),first) == row : Nat}:
41  match first:
42    case 0n: subtract_zero(row)
43    case 1n+rest: subtract_shift(rest,row)