def ends_self

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

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/arith.bend as NR

70# b <= f is enough: b drops every step
71def ends_self(+f: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(b, f) == True{} : Bool}) -> {ends(f, a, b) == True{} : Bool}:
72  match f b:
73    case _ 0n:
74      ends_zero(f, a)
75    case 0n 1n+bp:
76      Empty.absurd({ends(0n, a, 1n+bp) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
77    case 1n+ +g 1n+ +bp:
78      ends_self(g, 1n+bp, Nat.mod(a, 1n+bp), N.lt_succ_le(Nat.mod(a, 1n+bp), g, N.lt_le_trans(Nat.mod(a, 1n+bp), 1n+bp, 1n+g, NR.dm_lt(bp, a), h)))