compExactValue_correctness_of_stream_eq_some_aux_comp

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

Похожие утверждения