law max_lt

lawful-words@0.1.0.0 · proof_u32.bend:920

import Base

920law max_lt:
921  for +x: Nat
922  for +y: Nat
923  for +h: {Nat.is_lt(x, y) == True{} : Bool}
924  {Nat.max(x, y) == y : Nat}