law le_not_lt

lawful-words@0.1.0.0 · proof_nat.bend:1519

import Base

1519# a <= b gives not (b < a).
1520law le_not_lt:
1521  for +a: Nat
1522  for +b: Nat
1523  for +h: {Nat.is_le(a, b) == True{} : Bool}
1524  {Nat.is_lt(b, a) == False{} : Bool}