law not_is_le

bend-mathlib@0.8.1.0 · nat.bend:1372

import Base

1372# Not (a <= b) tests the same as b < a.
1373law not_is_le:
1374  for a: Nat
1375  for b: Nat
1376  {Bool.not(Nat.is_le(a, b)) == Nat.is_lt(b, a) : Bool}