def est_eq_n

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64est.bend:203

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as LW

203def est_eq_n(+y: WU.U64, +d: U32, +hd: {U32.is_zero(d) == False{} : Bool}, +n: Nat, +hn: {v(d) == n : Nat}) -> {X.est32(y, d) == X.q_clamp(X.fst_q(X.div32(y, d))) : U32}:
204  match n:
205    case 0n:
206      Empty.absurd({X.est32(y, d) == X.q_clamp(X.fst_q(X.div32(y, d))) : U32}, LW.true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(d), False{}, Equal.sym(Bool, U32.is_zero(d), True{}, Equal.trans(Bool, U32.is_zero(d), Nat.is_eq(v(d), 0n), True{}, LW.zero_nat(d), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(d), 0n, hn))), hd)))
207    case 1n+ +bp:
208      est_eq_c(y, d, hd, bp, hn, U32.is_le(d, X.hi(y)), {==})