law not_lt_of_le

bend-mathlib@0.8.1.0 · nat.bend:1602

import Base

1602# A weak inequality rules out the reverse strict one: a <= b implies b < a is false.
1603law not_lt_of_le:
1604  for a: Nat
1605  for b: Nat
1606  for h: le(a, b)
1607  {Nat.is_lt(b, a) == False{} : Bool}