~/jendhub

def min_le_right

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

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

45def min_le_right(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}:
46  match a b:
47    case 0n _:
48      Arith.le_zero(b)
49    case 1n+p 0n:
50      {==}
51    case 1n+p 1n+q:
52      min_le_right(p, q)

Uses (5)

Used by (1)