case pp
a n : ℕ
⊢ Function.Periodic (coprime a) a
a n : ℕ
⊢ card (filter (coprime a) (Ico n (n + a))) = φ a
rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range]
no goals
case pp
a n : ℕ
⊢ Function.Periodic (coprime a) a
exact periodic_coprime a