Documentation

Lean 4 Proof

theorem debtSustainable_requires_surplus {r_B g b d : ℝ}
    (hrg : g < r_B) (hb : 0 < b) (hsust : debtSustainable r_B g b d) :
    d < 0 := by
  rw [debtSustainable_iff] at hsust
  have : (g - r_B) * b < 0 := mul_neg_of_neg_of_pos (by linarith) hb
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:370

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file