def min_le_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:90

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

90def min_le_r(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), b) == True{} : Bool}:
91  match a b:
92    case 0n _:
93      N.zero_le(b)
94    case 1n+ +ap 0n:
95      {==}
96    case 1n+ +ap 1n+ +bp:
97      min_le_r(ap, bp)