English
If c < a, then (a · b + c) / (a · d) = b / d.
Русский
Если c < a, то (a · b + c) / (a · d) = b / d.
LaTeX
$$$c \\\\lt a \\\\Rightarrow \\\\frac{a \\\\cdot b + c}{a \\\\cdot d} = \\frac{b}{d}$$$
Lean4
theorem mul_add_div_mul {a c : Ordinal} (hc : c < a) (b d : Ordinal) : (a * b + c) / (a * d) = b / d :=
by
have ha : a ≠ 0 := ((Ordinal.zero_le c).trans_lt hc).ne'
obtain rfl | hd := eq_or_ne d 0
· rw [mul_zero, div_zero, div_zero]
· have H := mul_ne_zero ha hd
apply le_antisymm
· rw [← lt_succ_iff, div_lt H, mul_assoc]
· apply (add_lt_add_left hc _).trans_le
rw [← mul_succ]
apply mul_le_mul_left'
rw [succ_le_iff]
exact lt_mul_succ_div b hd
· rw [le_div H, mul_assoc]
exact (mul_le_mul_left' (mul_div_le b d) a).trans (le_add_right _ c)
