rw [←Subtype.coe_lt_coe, Positive.coe_add]
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ⟨c, hc⟩ < ⟨b, hb⟩ + ⟨c, hc⟩
case mk.mk
a : ℝ+
b : ℝ
hb : 0 < b
c : ℝ
hc : 0 < c
h : a = ⟨b, hb⟩ + ⟨c, hc⟩
⊢ ↑⟨c, hc⟩ < ↑⟨b, hb⟩ + ↑⟨c, hc⟩