def sub_split

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:29

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

29# d < n: n - d == 1 + (n - (d + 1))
30def sub_split(+n: Nat, +d: Nat, +h: {Nat.is_lt(d, n) == True{} : Bool}) -> {Nat.sub(n, d) == 1n+Nat.sub(n, 1n+d) : Nat}:
31  match n d:
32    case 0n _:
33      Empty.absurd({Nat.sub(0n, d) == 1n+Nat.sub(0n, 1n+d) : Nat}, N.lt_zero_absurd(d, h))
34    case 1n+ +np 0n:
35      %Equal.sym(Nat, Nat.sub(np, 0n), np, N.sub_zero(np)) : {1n+np == 1n+_ : Nat}
36      {==}
37    case 1n+ +np 1n+ +dp:
38      sub_split(np, dp, h)