have h5 : c / (b + c + d) < c / (c + d) :=
   div_lt_div_of_pos_left hc (add_pos hc hd) (by linarith)
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2
case intro.intro.intro.intro.intro.intro.intro.intro.right
a b c d : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
hd : 0 < d
h3 : a / (a + b + d) < a / (a + b)
h4 : b / (a + b + c) < b / (a + b)
h5 : c / (b + c + d) < c / (c + d)
⊢ a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d) < 2