def max_le

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:61

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

61def max_le(+a: Nat, +b: Nat, +h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.max(a, b) == b : Nat}:
62  match a b:
63    case 0n _:
64      {==}
65    case 1n+ +ap 0n:
66      Empty.absurd({Nat.max(1n+ap, 0n) == 0n : Nat}, LW.true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
67    case 1n+ +ap 1n+ +bp:
68      Equal.cong(Nat, Nat, z => 1n+z, Nat.max(ap, bp), bp, max_le(ap, bp, h))