Documentation

Lean 4 Proof

theorem more_heirs_lower_herfindahl {N₁ N₂ : ℕ} (hN₁ : 0 < N₁) (h : N₁ < N₂) :
    bequestHerfindahl N₂ < bequestHerfindahl N₁ := by
  simp only [bequestHerfindahl]
  apply div_lt_div_of_pos_left one_pos
  · exact Nat.cast_pos.mpr hN₁
  · exact_mod_cast h

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:148

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file