Theorem: Choose_self_eq_one (BrownCs22/Homework/Hw8.lean)

State before:
n : ℕ
⊢ (n C n) = 1
Tactic:
sorry
State after:
no goals