-- Reproduction axiom trail -- re-derived from source (TOOLCHAIN tier).
-- theorem : MachLib.Finance.days30E360_additive
-- source  : MachLib.FinanceDayCount   (machlib module; the theorem's own #print axioms)
-- tool    : forge e914e8d . machlib f3d5490 . lean via lake
-- when    : 2026-07-02T08:57:45Z
-- verdict : CLEAN -- footprint free of sorry- and classical-citation axioms
-- (re-derive: make verify-proof)
--
'MachLib.Finance.days30E360_additive' depends on axioms: [propext, Quot.sound]