def bends_self

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:165

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

165# n <= f is enough (n drops every step)
166def bends_self(+f: Nat, +n: Nat, +h: {Nat.is_le(n, f) == True{} : Bool}) -> {bends(f, n) == True{} : Bool}:
167  match f n:
168    case _ 0n:
169      bends_zero(f)
170    case 0n 1n+np:
171      Empty.absurd({bends(0n, 1n+np) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
172    case 1n+ +g 1n+ +np:
173      bends_self(g, Nat.div(1n+np, 2n), N.lt_succ_le(Nat.div(1n+np, 2n), g, N.lt_le_trans(Nat.div(1n+np, 2n), 1n+np, 1n+g, BT.half_lt(np), h)))