law sub_lt_dbl

lawful-words@0.1.0.0 · proof_u32.bend:701

import Base

701# x < 2b and b <= x give x - b < b.
702law sub_lt_dbl:
703  for +x: Nat
704  for +b: Nat
705  for +h1: {Nat.is_lt(x, Nat.double(b)) == True{} : Bool}
706  for +h2: {Nat.is_le(b, x) == True{} : Bool}
707  {Nat.is_lt(Nat.sub(x, b), b) == True{} : Bool}