law max_eq_right

bend-mathlib@0.8.1.0 · nat.bend:2425

import Base

2425# The maximum is the larger argument on the right: a <= b implies max a b = b.
2426law max_eq_right:
2427  for a: Nat
2428  for b: Nat
2429  for h: le(a, b)
2430  {Nat.max(a, b) == b : Nat}