law lt_of_le

lawful-bytes@0.1.1.0 · proof_same.bend:83

import Base

83# a + 1 + m <= b gives a < b.
84law lt_of_le:
85  for +a: Nat
86  for +m: Nat
87  for +b: Nat
88  for +h: {Nat.is_le(Nat.add(a, 1n+m), b) == True{} : Bool}
89  {Nat.is_lt(a, b) == True{} : Bool}