law le_iff_lt_or_eq_sym

bend-mathlib@0.8.1.0 · nat.bend:4590

import Base

4590# At most means below or equal: a <= b tests as a < b or a = b, reversed to rewrite toward the simple side.
4591law le_iff_lt_or_eq_sym:
4592  for a: Nat
4593  for b: Nat
4594  {Bool.or(Nat.is_lt(a, b), Nat.is_eq(a, b)) == Nat.is_le(a, b) : Bool}