def max_pick

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

import Base

293def max_pick(+a: Nat, +b: Nat) -> {Nat.max(a, b) == Bool.pick(Nat, Nat.is_le(a, b), b, a) : Nat}:
294  match a b:
295    case 0n 0n:
296      {==}
297    case 0n 1n+q:
298      {==}
299    case 1n+p 0n:
300      {==}
301    case 1n+p 1n+q:
302      Equal.trans(Nat, 1n+Nat.max(p, q), 1n+Bool.pick(Nat, Nat.is_le(p, q), q, p), Bool.pick(Nat, Nat.is_le(p, q), 1n+q, 1n+p),
303        Equal.cong(Nat, Nat, x => 1n+x, Nat.max(p, q), Bool.pick(Nat, Nat.is_le(p, q), q, p), max_pick(p, q)),
304        Equal.sym(Nat, Bool.pick(Nat, Nat.is_le(p, q), 1n+q, 1n+p), 1n+Bool.pick(Nat, Nat.is_le(p, q), q, p), pick_succ(Nat.is_le(p, q), q, p)))