def max_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addc.bend:42

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

42def max_le(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
43  match a b:
44    case 0n _:
45      {==}
46    case 1n+ +ap 0n:
47      NC.absurd_tf({Nat.max(1n+ap, 0n) == 0n : Nat}, h)
48    case 1n+ +ap 1n+ +bp:
49      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), bp, max_le(ap, bp, h))