-- Reproduction axiom trail -- re-derived from source (TOOLCHAIN tier).
-- theorem : MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional
-- source  : MachLib.ChainExp2NoZeros   (machlib module; the theorem's own #print axioms)
-- tool    : forge 8074510 . machlib 1420f96 . lean via lake
-- when    : 2026-07-02T04:37:24Z
-- verdict : CLEAN -- footprint free of sorry- and classical-citation axioms
-- (re-derive: make verify-proof)
--
'MachLib.ChainExp2NoZeros.chain2_khovanskii_bound_unconditional' depends on axioms: [propext,
 Classical.choice,
 MachLib.Real,
 Quot.sound,
 MachLib.Real.HasDerivAt,
 MachLib.Real.HasDerivAt_add,
 MachLib.Real.HasDerivAt_comp,
 MachLib.Real.HasDerivAt_const,
 MachLib.Real.HasDerivAt_exp,
 MachLib.Real.HasDerivAt_id,
 MachLib.Real.HasDerivAt_mul,
 MachLib.Real.HasDerivAt_sub,
 MachLib.Real.HasDerivAt_unique,
 MachLib.Real.addR,
 MachLib.Real.add_assoc,
 MachLib.Real.add_comm,
 MachLib.Real.add_lt_add_left,
 MachLib.Real.add_neg,
 MachLib.Real.add_zero,
 MachLib.Real.divR,
 MachLib.Real.exp,
 MachLib.Real.exp_pos,
 MachLib.Real.leR,
 MachLib.Real.le_iff_lt_or_eq,
 MachLib.Real.ltR,
 MachLib.Real.lt_irrefl_ax,
 MachLib.Real.lt_total,
 MachLib.Real.lt_trans_ax,
 MachLib.Real.mulR,
 MachLib.Real.mul_assoc,
 MachLib.Real.mul_comm,
 MachLib.Real.mul_distrib,
 MachLib.Real.mul_inv,
 MachLib.Real.mul_one_ax,
 MachLib.Real.natCast,
 MachLib.Real.natCast_succ,
 MachLib.Real.natCast_zero,
 MachLib.Real.negR,
 MachLib.Real.oneR,
 MachLib.Real.rolle,
 MachLib.Real.subR,
 MachLib.Real.sub_def,
 MachLib.Real.zeroR,
 MachLib.Real.zero_count_bound_by_deriv,
 MachLib.Real.zero_lt_one_ax,
 MachLib.Real.zero_ne_one_ax]