def min_le_l

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

import Base

99def min_le_l(+a: Nat, +b: Nat) -> {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}:
100  match a b:
101    case 0n _:
102      {==}
103    case 1n+ +ap 0n:
104      {==}
105    case 1n+ +ap 1n+ +bp:
106      min_le_l(ap, bp)