Theorem: card_Icc_one_n_n (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A B : Set ℕ
n✝ n : ℕ
⊢ (Icc 1 n).card = n
Tactic:
rw [Nat.card_Icc 1 n, add_tsub_cancel_right]
State after:
no goals