def min_left

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

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

25def min_left(+a: Nat, +b: Nat, h: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.min(a, b) == a : Nat}:
26  match a b:
27    case 0n _:
28      {==}
29    case 1n+p 0n:
30      Empty.absurd({Nat.min(1n+p, 0n) == 1n+p : Nat}, Arith.clash(h))
31    case 1n+p 1n+q:
32      Equal.cong(Nat, Nat, x => 1n+x, Nat.min(p, q), p, min_left(p, q, h))