English
A specialized auxiliary correctness lemma: for a, b, if fract a ≠ 0, then a*b + c over fract a equals (b*a + c)/fract a; i.e., two equivalent expressions match after simplification.
Русский
Специализированная вспомогательная лемма корректности: если дробная часть a ≠ 0, то \\\\frac{\\\\lfloor a\\\\rfloor b + c}{\\\\{fract a\\\\}} = \\\\frac{b a + c}{fract a}.
LaTeX
$$$\\\\forall {K} [Field K] [LinearOrder K] [FloorRing K] {a b c : K}, \\\\text{fract } a \\\\neq 0 \\\\Rightarrow \\\\frac{\\\\lfloor a\\\\rfloor b + c}{\\\\text{fract } a} + b = \\\\frac{b a + c}{\\\\text{fract } a}$$$
Lean4
/-- Just a computational lemma we need for the next main proof. -/
protected theorem compExactValue_correctness_of_stream_eq_some_aux_comp {a : K} (b c : K)
(fract_a_ne_zero : Int.fract a ≠ 0) : ((⌊a⌋ : K) * b + c) / Int.fract a + b = (b * a + c) / Int.fract a :=
by
field_simp
rw [Int.fract]
ring