proposition: Theorem binomial2 : forall n : nat, power 2 n = sum_nm 0 n (fun x => binomial n x).
proof: Proof. intros n; replace 2 with (1 + 1); auto with arith. rewrite exp_Pascal. apply sum_nm_ext. intros x H; repeat rewrite SO_power || rewrite Nat.mul_1_r; auto. Qed.
imports: Coq(Arith ArithRing Wf_nat)