Documentation

Lean 4 Proof

theorem minimum_heirs_for_exemption {W E₀ : ℝ} {N : ℕ}
    (_hE : 0 < E₀) (hN : 0 < N) (_hW : 0 ≤ W)
    (h : W ≤ E₀ * ↑N) :
    perHeirWealth W N ≤ E₀ := by
  simp only [perHeirWealth]
  rw [div_le_iff₀ (Nat.cast_pos.mpr hN)]
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/FairInheritance.lean:344

Module Section

Fair Inheritance: Taxing Concentration, Not Transfer

In the same file