def max_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:633

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC

633def max_l(+a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.max(a, b) == a : Nat}:
634  match a b:
635    case 0n 0n:
636      {==}
637    case 0n 1n+ +bp:
638      NC.absurd_tf({Nat.max(0n, 1n+bp) == 0n : Nat}, h)
639    case 1n+ +ap 0n:
640      {==}
641    case 1n+ +ap 1n+ +bp:
642      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), ap, max_l(ap, bp, h))