LeanPool.DirectedTopologyLean4.FractionEqualities

theorem FractionEqualities.one_sub_inverse_of_add_one {n : ℝ} (hn : n + 1 ≠ 0) : 1 - 1 / (n + 1) = n / (n + 1)

theorem FractionEqualities.frac_cancel {a b c : ℝ} (hb : b ≠ 0) : a / b * (b / c) = a / c

theorem FractionEqualities.frac_cancel' {a b c : ℝ} (hb : b ≠ 0) : b / a * (c / b) = c / a

theorem FractionEqualities.one_sub_frac {a b : ℝ} (hb : b + 1 ≠ 0) : 1 - (a + 1) / (b + 1) = (b - a) / (b + 1)

theorem FractionEqualities.frac_special {a b c : ℝ} (hbc : b ≠ c) (hc : c + 1 ≠ 0) : (a + (b + 1)) / (c + 1) = (1 - (b + 1) / (c + 1)) * (a / (c - b)) + (b + 1) / (c + 1)

theorem FractionEqualities.cancel_common_factor {i n : ℕ} (i_pos : 0 < i) (hi_n : (i - 1).succ ≤ ((n + 1) * i - 1).succ) : Fraction.ofPos ⋯ = Fraction ⋯ hi_n

For any i n : ℕ with i > 0 and i ≤ (n + 1) * i, we have that 1 / (n + 1) = i / ((n + 1) * i).