law le_split

lawful-bytes@0.1.1.0 · proof_append.bend:116

import Base

116law le_split:
117  for +a: Nat
118  for +k: Nat
119  for +m: Nat
120  for +h: {Nat.is_le(Nat.add(a, 1n+k), m) == True{} : Bool}
121  {Nat.is_lt(a, m) == True{} : Bool}