law lt_sub

lawful-arrays@0.1.0.0 · proof_base.bend:186

import Base

186# k is at least m and below m + m2, so k - m is below m2.
187law lt_sub:
188  for +m: Nat
189  for +k: Nat
190  for +m2: Nat
191  for h1: {Nat.is_lt(k, m) == False{} : Bool}
192  for h2: {Nat.is_lt(k, Nat.add(m, m2)) == True{} : Bool}
193  {Nat.is_lt(Nat.sub(k, m), m2) == True{} : Bool}