def le

bend-mathlib@0.8.1.0 · nat.bend:339

import Base

339# The order a <= b on naturals, as a reusable proposition.
340def le(a: Nat, b: Nat) -> Data:
341  {Nat.is_le(a, b) == True{} : Bool}