def le_succ_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:655

import Base

655def le_succ_lt(+a: Nat, +b: Nat) -> {Nat.is_le(1n+a, b) == Nat.is_lt(a, b) : Bool}:
656  match a b:
657    case 0n 0n:
658      {==}
659    case 0n 1n+ +bp:
660      match bp:
661        case 0n:
662          {==}
663        case 1n+ +bq:
664          {==}
665    case 1n+ +ap 0n:
666      {==}
667    case 1n+ +ap 1n+ +bp:
668      le_succ_lt(ap, bp)