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