law not_is_lt_sym

bend-mathlib@0.8.1.0 · nat.bend:4292

import Base

4292# Not (a < b) tests the same as b <= a, reversed to rewrite toward the simple side.
4293law not_is_lt_sym:
4294  for a: Nat
4295  for b: Nat
4296  {Nat.is_le(b, a) == Bool.not(Nat.is_lt(a, b)) : Bool}