law not_is_le_sym

bend-mathlib@0.8.1.0 · nat.bend:4283

import Base

4283# Not (a <= b) tests the same as b < a, reversed to rewrite toward the simple side.
4284law not_is_le_sym:
4285  for a: Nat
4286  for b: Nat
4287  {Nat.is_lt(b, a) == Bool.not(Nat.is_le(a, b)) : Bool}