law lt_not_le

lawful-words@0.1.0.0 · proof_bytes.bend:398

import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytes
import Base

398law lt_not_le:
399  for +x: Nat
400  for +y: Nat
401  for +h: {Nat.is_lt(x, y) == True{} : Bool}
402  {Nat.is_le(y, x) == False{} : Bool}

Uses (9)

Used by (3)