def fst_b
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend as Logsimport Base
85# b^ilog(n, b) <= n (Mathlib Nat.pow_log_le_self)
86def fst_b(-P: Type, -Q: Type, p: P & Q) -> P:
87 (a, b) = p
88 a
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/logs.bend as Logsimport Base
85# b^ilog(n, b) <= n (Mathlib Nat.pow_log_le_self)
86def fst_b(-P: Type, -Q: Type, p: P & Q) -> P:
87 (a, b) = p
88 a