def lt_succ_split

bend-collections-laws-math@1.0.0.0 · proofs/math/random/shuffle.bend:118

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

118# [p == v] + [v < p] == [v < p + 1]
119def lt_succ_split(+v: Nat, +p: Nat) -> {Nat.add(SR.b2n(Nat.is_eq(p, v)), SR.b2n(Nat.is_lt(v, p))) == SR.b2n(Nat.is_lt(v, 1n+p)) : Nat}:
120  match v p:
121    case 0n 0n:
122      {==}
123    case 0n 1n+q:
124      {==}
125    case 1n+u 0n:
126      %Equal.sym(Bool, Nat.is_lt(u, 0n), False{}, N.not_lt_zero(u)) : {0n == SR.b2n(_) : Nat}
127      {==}
128    case 1n+u 1n+q:
129      lt_succ_split(u, q)