def le_nlt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:137

import Base

137def le_nlt(+a: Nat, +b: Nat) -> {Nat.is_le(a, b) == Bool.not(Nat.is_lt(b, a)) : Bool}:
138  match a b:
139    case 0n 0n:
140      {==}
141    case 0n 1n+ +bp:
142      {==}
143    case 1n+ +ap 0n:
144      {==}
145    case 1n+ +ap 1n+ +bp:
146      le_nlt(ap, bp)