def sub_back

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:121

import Base

121# stop - low = 1 + rest gives stop = low + (1 + rest).
122def sub_back(+stop: Nat, +low: Nat, +rest: Nat, e: {Nat.sub(stop, low) == 1n+rest : Nat}) -> {Nat.add(low, 1n+rest) == stop : Nat}:
123  match stop low:
124    case 0n _:
125      Empty.absurd({Nat.add(low, 1n+rest) == 0n : Nat}, nat_clash(rest, Equal.sym(Nat, 0n, 1n+rest, e)))
126    case 1n+ap 0n:
127      Equal.sym(Nat, 1n+ap, 1n+rest, e)
128    case 1n+ap 1n+lp:
129      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(lp, 1n+rest), ap, sub_back(ap, lp, rest, e))