law le_iff_lt_or_eq

bend-mathlib@0.8.1.0 · nat.bend:2623

import Base

2623# At most means below or equal: a <= b tests as a < b or a = b.
2624law le_iff_lt_or_eq:
2625  for a: Nat
2626  for b: Nat
2627  {Nat.is_le(a, b) == Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)) : Bool}