law max_nlt

lawful-words@0.1.0.0 · proof_u32.bend:935

import Base

935law max_nlt:
936  for +x: Nat
937  for +y: Nat
938  for +h: {Nat.is_lt(x, y) == False{} : Bool}
939  {Nat.max(x, y) == x : Nat}