def below_successor

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/division_quotient.bend:14

import Base

14def below_successor(r: Nat, p: Nat) -> {Nat.is_lt(r, 1n+p) == Nat.is_le(r, p) : Bool}:
15  match r p:
16    case 0n 0n: {==}
17    case 0n 1n+k: {==}
18    case 1n+0n 0n: {==}
19    case 1n+1n+j 0n: {==}
20    case 1n+k 1n+j: below_successor(k, j)