~/jendhub

law le_of_is_lt

bend-lawful-stdlib@0.1.0.0 · src/nat.bend:132

import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat
import Base

132# The two outcomes of Nat.is_lt as LE proofs. Base's min, max and clamp
133# branch on is_lt.
134law le_of_is_lt:
135  for a: Nat
136  for b: Nat
137  for e: {Nat.is_lt(a, b) == True{} : Bool}
138  LE(a, b)

Uses (6)

Used by (1)