law succ_le

lawful-bytes@0.1.1.0 · proof_core.bend:543

import Base

543law succ_le:
544  for +x: Nat
545  for +m: Nat
546  for +h: {Nat.is_lt(x, m) == True{} : Bool}
547  {Nat.is_le(Nat.add(x, 1n), m) == True{} : Bool}