m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Nat.gcd (Int.natAbs (-(m ^ 2 - n ^ 2))) (Int.natAbs (2 * m * n)) = 1
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1
rw [Int.gcd, ← Int.natAbs_neg (m ^ 2 - n ^ 2)]
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Nat.gcd (Int.natAbs (n ^ 2 - m ^ 2)) (Int.natAbs (2 * n * m)) = 1
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Nat.gcd (Int.natAbs (-(m ^ 2 - n ^ 2))) (Int.natAbs (2 * m * n)) = 1
rw [(by ring : 2 * m * n = 2 * n * m), (by ring : -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2)]
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Int.gcd n m = 1
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Nat.gcd (Int.natAbs (n ^ 2 - m ^ 2)) (Int.natAbs (2 * n * m)) = 1
apply coprime_sq_sub_mul_of_even_odd _ hn hm
no goals
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ Int.gcd n m = 1
rwa [Int.gcd_comm]
no goals
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ 2 * m * n = 2 * n * m
ring
no goals
m n : ℤ
h : Int.gcd m n = 1
hm : m % 2 = 1
hn : n % 2 = 0
⊢ -(m ^ 2 - n ^ 2) = n ^ 2 - m ^ 2
ring