def min_mono

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

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

54# min(a, b) <= min(c, b) for a <= c.
55def min_mono(+a: Nat, +c: Nat, +b: Nat, h: {Nat.is_le(a, c) == True{} : Bool}) -> {Nat.is_le(Nat.min(a, b), Nat.min(c, b)) == True{} : Bool}:
56  match a c b:
57    case 0n _ _:
58      Arith.le_zero(Nat.min(c, b))
59    case 1n+p 0n _:
60      Empty.absurd({Nat.is_le(Nat.min(1n+p, b), Nat.min(0n, b)) == True{} : Bool}, Arith.clash(h))
61    case 1n+p 1n+q 0n:
62      {==}
63    case 1n+p 1n+q 1n+r:
64      min_mono(p, q, r, h)