law not_le_of_lt

bend-mathlib@0.8.1.0 · nat.bend:1584

import Base

1584# A strict inequality rules out the reverse weak one: a < b implies b <= a is false.
1585law not_le_of_lt:
1586  for a: Nat
1587  for b: Nat
1588  for h: lt(a, b)
1589  {Nat.is_le(b, a) == False{} : Bool}