def positive_difference

stelliferous@0.0.2.0 · proofs/nat_order.bend:57

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

57def positive_difference(+end: Nat,+begin: Nat,positive: {Nat.is_lt(begin,end) == True{} : Bool}) -> {Nat.is_lt(0n,Nat.sub(end,begin)) == True{} : Bool}:
58  match end begin:
59    case 0n 0n: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
60    case 0n 1n+begin: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(positive))
61    case 1n+end 0n: {==}
62    case 1n+end 1n+begin: positive_difference(end,begin,positive)