def max_eq_l

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/misc.bend:36

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

36def max_eq_l(+x: Nat, +lo: Nat, +h: {Nat.is_le(lo, x) == True{} : Bool}) -> {Nat.max(x, lo) == x : Nat}:
37  match x lo:
38    case 0n 0n:
39      {==}
40    case 0n 1n+lp:
41      Empty.absurd({Nat.max(0n, 1n+lp) == 0n : Nat}, L.false_true(h))
42    case 1n+xp 0n:
43      {==}
44    case 1n+ +xp 1n+ +lp:
45      N.succ_cong(Nat.max(xp, lp), xp, max_eq_l(xp, lp, h))