law le_of_not_lt

bend-mathlib@0.8.1.0 · nat.bend:1638

import Base

1638# A failed strict test gives the reverse weak order: a < b false implies b <= a.
1639law le_of_not_lt:
1640  for a: Nat
1641  for b: Nat
1642  for h: {Nat.is_lt(a, b) == False{} : Bool}
1643  le(b, a)