a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a < 1
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 1 < 1 / a
rw [lt_div_iff ha, one_mul]
no goals
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a < 1
linarith
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a + b = 1
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 1 / (1 / a) + 1 / (1 / b) = 1
simp_rw [one_div_one_div]
no goals
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a + b = 1
exact hab