def restore_shift

stelliferous@0.0.2.0 · proofs/nat_order.bend:45

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

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