[STATEMENT]
lemma sum_choose_upper: "(\<Sum>k\<le>n. k choose m) = Suc n choose Suc m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<le>n. k choose m) = Suc n choose Suc m
[PROOF STEP]
by (induct n) auto