law lt_of_not_le

bend-mathlib@0.8.1.0 · nat.bend:1620

import Base

1620# A failed weak test gives the reverse strict order: a <= b false implies b < a.
1621law lt_of_not_le:
1622  for a: Nat
1623  for b: Nat
1624  for h: {Nat.is_le(a, b) == False{} : Bool}
1625  lt(b, a)