Documentation

Lean 4 Proof

theorem profitShare_decreasing {Jσ₁ Jσ₂ : ℝ}
    (hJσ₁ : 0 < Jσ₁) (_hJσ₂ : 0 < Jσ₂) (hJσ : Jσ₁ < Jσ₂) :
    profitShare Jσ₂ < profitShare Jσ₁ := by
  simp only [profitShare]
  exact div_lt_div_of_pos_left one_pos hJσ₁ hJσ

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:176

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file