def le_max_r

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/misc.bend:27

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

27def le_max_r(+x: Nat, +lo: Nat) -> {Nat.is_le(lo, Nat.max(x, lo)) == True{} : Bool}:
28  match x lo:
29    case 0n l0:
30      N.le_refl(l0)
31    case 1n+xp 0n:
32      {==}
33    case 1n+ +xp 1n+ +lp:
34      le_max_r(xp, lp)