def max_of_ge

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32.bend:50

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/lemmas/spec/numeric.bend as S

50def max_of_ge(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.max(a, b) == a : Nat}:
51  match a b:
52    case 0n 0n:
53      {==}
54    case 0n 1n+bp:
55      Empty.absurd({Nat.max(0n, 1n+bp) == 0n : Nat}, N.zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
56    case 1n+ap 0n:
57      {==}
58    case 1n+ap 1n+bp:
59      N.succ_cong(Nat.max(ap, bp), ap, max_of_ge(ap, bp, h))