law max_eq_left

bend-mathlib@0.8.1.0 · nat.bend:2406

import Base

2406# The maximum is the larger argument on the left: b <= a implies max a b = a.
2407law max_eq_left:
2408  for a: Nat
2409  for b: Nat
2410  for h: le(b, a)
2411  {Nat.max(a, b) == a : Nat}