~/jendhub

def minimum_left

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:38

import stelliferous@0.0.2.0/proofs/nat_extrema.bend as NatExtrema
import Base

38def minimum_left(+left: Nat,+right: Nat) -> {Nat.is_le(Nat.min(left,right),left) == True{} : Bool}:
39  match left right:
40    case 0n right: {==}
41    case 1n+left 0n: {==}
42    case 1n+left 1n+right: minimum_left(left,right)

Uses (4)

Used by (1)