def max_le1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:113

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

113def max_le1(+b: Nat, +l: Nat, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {Nat.is_le(Nat.max(b, Nat.min(l, 1n)), 1n) == True{} : Bool}:
114  match b l:
115    case 0n 0n:
116      {==}
117    case 0n 1n+ +lp:
118      match lp:
119        case 0n:
120          {==}
121        case 1n+ +lq:
122          {==}
123    case 1n 0n:
124      {==}
125    case 1n 1n+ +lp:
126      match lp:
127        case 0n:
128          {==}
129        case 1n+ +lq:
130          {==}
131    case 2n+ +q _:
132      NC.absurd_tf({Nat.is_le(Nat.max(2n+q, Nat.min(l, 1n)), 1n) == True{} : Bool}, hb)