law le_lt_trans

lawful-words@0.1.0.0 · proof_nat.bend:756

import Base

756law le_lt_trans:
757  for +a: Nat
758  for +b: Nat
759  for +c: Nat
760  for ab: {Nat.is_le(a, b) == True{} : Bool}
761  for bc: {Nat.is_lt(b, c) == True{} : Bool}
762  {Nat.is_lt(a, c) == True{} : Bool}