law lt_le_trans

lawful-words@0.1.0.0 · proof_nat.bend:744

import Base

744law lt_le_trans:
745  for +a: Nat
746  for +b: Nat
747  for +c: Nat
748  for ab: {Nat.is_lt(a, b) == True{} : Bool}
749  for bc: {Nat.is_le(b, c) == True{} : Bool}
750  {Nat.is_lt(a, c) == True{} : Bool}