m n : ℕ
⊢ ↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + (↑n + 1) * Nat.gcdB (natAbs ↑m) (Nat.succ n)
m n : ℕ
⊢ ↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + -(↑n + 1) * -Nat.gcdB (natAbs ↑m) (Nat.succ n)
rw [neg_mul_neg]
no goals
m n : ℕ
⊢ ↑(gcd ↑m -[n+1]) = ↑m * gcdA ↑m -[n+1] + (↑n + 1) * Nat.gcdB (natAbs ↑m) (Nat.succ n)
apply Nat.gcd_eq_gcd_ab
m n : ℕ
⊢ ↑(gcd -[m+1] ↑n) = (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
m n : ℕ
⊢ ↑(gcd -[m+1] ↑n) = -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
rw [neg_mul_neg]
no goals
m n : ℕ
⊢ ↑(gcd -[m+1] ↑n) = (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs ↑n) + ↑n * gcdB -[m+1] ↑n
apply Nat.gcd_eq_gcd_ab
m n : ℕ
⊢ ↑(gcd -[m+1] -[n+1]) =
    (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + (↑n + 1) * Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
m n : ℕ
⊢ ↑(gcd -[m+1] -[n+1]) =
    -(↑m + 1) * -Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + -(↑n + 1) * -Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
rw [neg_mul_neg, neg_mul_neg]
no goals
m n : ℕ
⊢ ↑(gcd -[m+1] -[n+1]) =
    (↑m + 1) * Nat.gcdA (Nat.succ m) (natAbs -[n+1]) + (↑n + 1) * Nat.gcdB (natAbs -[m+1]) (Nat.succ n)
apply Nat.gcd_eq_gcd_ab