def min_right

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:544

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

544def min_right(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.min(a, b) == b : Nat}:
545  match a b:
546    case 0n 0n:
547      {==}
548    case 0n 1n+bp:
549      Empty.absurd({Nat.min(0n, 1n+bp) == 1n+bp : Nat}, zero_succ(0n, Equal.sym(Nat, 1n, 0n, Equal.cong(Bool, Nat, c => S.bit_value(c), True{}, False{}, h))))
550    case 1n+ap 0n:
551      {==}
552    case 1n+ap 1n+bp:
553      succ_cong(Nat.min(ap, bp), bp, min_right(ap, bp, h))