English
Nat.xgcdAux satisfies a preservation property P under successor steps: if P holds for (r,s,t) and (r',s',t'), then P holds for xgcdAux r s t r' s' t'.
Русский
Nat.xgcdAux удовлетворяет сохранению свойства P при переходах к следующему шагу: если P выполняется для (r,s,t) и (r',s',t'), тогда P выполняется для xgcdAux r s t r' s' t'.
LaTeX
$$$\forall r,r',\,\forall s,t,s',t',\; P(x,y,(r,s,t)) \rightarrow P(x,y,(r',s',t')) \rightarrow P(x,y,(xgcdAux\,r\,s\,t\,r'\,s'\,t'))$$$
Lean4
@[simp]
theorem xgcdAux_fst (x y) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
gcd.induction x y (by simp) fun x y h IH s t s' t' =>
by
simp only [h, xgcdAux_rec, IH]
rw [← gcd_rec]
