def max_r

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

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

624def max_r(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
625  match a b:
626    case 0n _:
627      {==}
628    case 1n+ +ap 0n:
629      NC.absurd_tf({Nat.max(1n+ap, 0n) == 0n : Nat}, h)
630    case 1n+ +ap 1n+ +bp:
631      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), bp, max_r(ap, bp, h))