law not_le_lt

lawful-words@0.1.0.0 · proof_nat.bend:693

import lawful-words@0.1.0.0/proof_nat.bend as ProofNat
import Base

693# not (a <= b) is b < a.
694law not_le_lt:
695  for +a: Nat
696  for +b: Nat
697  for e: {Nat.is_le(a, b) == False{} : Bool}
698  {Nat.is_lt(b, a) == True{} : Bool}

Uses (9)

Used by (5)