def min_pick

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:280

import Base

280def min_pick(+a: Nat, +b: Nat) -> {Nat.min(a, b) == Bool.pick(Nat, Nat.is_le(a, b), a, b) : Nat}:
281  match a b:
282    case 0n 0n:
283      {==}
284    case 0n 1n+q:
285      {==}
286    case 1n+p 0n:
287      {==}
288    case 1n+p 1n+q:
289      Equal.trans(Nat, 1n+Nat.min(p, q), 1n+Bool.pick(Nat, Nat.is_le(p, q), p, q), Bool.pick(Nat, Nat.is_le(p, q), 1n+p, 1n+q),
290        Equal.cong(Nat, Nat, x => 1n+x, Nat.min(p, q), Bool.pick(Nat, Nat.is_le(p, q), p, q), min_pick(p, q)),
291        Equal.sym(Nat, Bool.pick(Nat, Nat.is_le(p, q), 1n+p, 1n+q), 1n+Bool.pick(Nat, Nat.is_le(p, q), p, q), pick_succ(Nat.is_le(p, q), p, q)))