def max_ge_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:161

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

161def max_ge_l(+a: Nat, +b: Nat) -> {Nat.is_le(a, Nat.max(a, b)) == True{} : Bool}:
162  match a b:
163    case 0n _:
164      N.zero_le(b)
165    case 1n+ +ap 0n:
166      N.le_refl(1n+ap)
167    case 1n+ +ap 1n+ +bp:
168      max_ge_l(ap, bp)