def sum_bound

stelliferous@0.0.2.0 · proofs/binary_division.bend:98

import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

98def sum_bound(+s: Nat,+b: Nat,h: {Nat.is_lt(s,Nat.double(b)) == True{} : Bool}) -> {Nat.is_lt(s,Nat.add(b,b)) == True{} : Bool}:
99  %Equal.sym(Nat,Nat.add(b,b),Nat.double(b),Addition.double(b)) : {Nat.is_lt(s,_) == True{} : Bool}
100  h