def sub_odd

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64adds.bend:66

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

66def sub_odd(+t: Nat, +k: Nat, +hk: {Nat.is_lt(k, t) == True{} : Bool}) -> {Nat.is_eq(Nat.sub(Nat.double(t), 1n+Nat.double(k)), 0n) == False{} : Bool}:
67  match t k:
68    case 0n _:
69      Empty.absurd({Nat.is_eq(Nat.sub(0n, 1n+Nat.double(k)), 0n) == False{} : Bool}, N.lt_zero_absurd(k, hk))
70    case 1n+ +tp 0n:
71      {==}
72    case 1n+ +tp 1n+ +kp:
73      sub_odd(tp, kp, hk)