xgcdAux_P — Mathlib

English

Same invariant as 97947, expressing the P-preservation property for xgcdAux under the two-argument progression.

Русский

То же самое инвариант, что и в 97947, выражающий сохранение свойства P на продолжении xgcdAux.

LaTeX

$$$\forall r,r' : \mathbb{N}, \forall s,t,s',t' : \mathbb{Z},\; P(x,y,(r,s,t)) \rightarrow P(x,y,(r',s',t')) \rightarrow P(x,y,(r.xgcdAux s t r' s' t'))$$$

Lean4

theorem xgcdAux_P {r r'} : ∀ {s t s' t'}, P x y (r, s, t) → P x y (r', s', t') → P x y (xgcdAux r s t r' s' t') := by
  induction r, r' using gcd.induction with
  | H0 => simp
  | H1 a b h IH =>
    intro s t s' t' p p'
    rw [xgcdAux_rec h]; refine IH ?_ p; dsimp [P] at *
    rw [Int.emod_def]; generalize (b / a : ℤ) = k
    rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t, mul_comm k s, ← mul_assoc, ←
      mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]

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