law nat_lt_le_trans
import lawful-words@0.1.0.0/LAWS.bend as LAWSimport Base
538law nat_lt_le_trans:
539 for a: Nat
540 for b: Nat
541 for c: Nat
542 for h1: {Nat.is_lt(a, b) == True{} : Bool}
543 for h2: {Nat.is_le(b, c) == True{} : Bool}
544 {Nat.is_lt(a, c) == True{} : Bool}
Uses (5)
Used by (0)
No other definition uses this definition.