law not_lt_le

lawful-words@0.1.0.0 · proof_nat.bend:675

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

675# not (a < b) is b <= a.
676law not_lt_le:
677  for +a: Nat
678  for +b: Nat
679  for e: {Nat.is_lt(a, b) == False{} : Bool}
680  {Nat.is_le(b, a) == True{} : Bool}

Uses (6)

Used by (10)