NatOrder.restore_shift: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder
Lines 45-50 of stelliferous@0.0.2.0/proofs/nat_order.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&start_line=45&end_line=50

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

def restore_shift(+first: Nat,+row: Nat,lower: {Nat.is_le(first,row) == True{} : Bool}) -> {Nat.add(first,Nat.sub(row,first)) == row : Nat}:
  match first row:
    case 0n row: subtract_zero(row)
    case 1n+first 0n: Empty.absurd({Nat.add(1n+first,Nat.sub(0n,1n+first)) == 0n : Nat},WordEncoding.false_true(lower))
    case 1n+ +first 1n+ +row:
      Equal.cong(Nat,Nat,n => 1n+n,Nat.add(first,Nat.sub(row,first)),row,restore_shift(first,row,lower))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=subtract_zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=false_true