n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
n d : ℕ
n_coprime_d : coprime n d
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
have : (n : ℤ) % d = n - d * ⌊(n : ℚ) / d⌋ := Int.mod_nat_eq_sub_mul_floor_rat_div
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n % ↑d)) d
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n - ↑d * ⌊↑n / ↑d⌋)) d
rw [← this]
n d : ℕ
n_coprime_d : coprime n d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : coprime d n
⊢ coprime (natAbs (↑n % ↑d)) d
n d : ℕ
n_coprime_d : coprime n d
this : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
⊢ coprime (natAbs (↑n % ↑d)) d
have : d.coprime n := n_coprime_d.symm
no goals
n d : ℕ
n_coprime_d : coprime n d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : coprime d n
⊢ coprime (natAbs (↑n % ↑d)) d
rwa [Nat.coprime, Nat.gcd_rec] at this