Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active Aug 29, 2015
Embed
What would you like to do?
Require Import NArith.
Fixpoint sum_of (f : nat -> nat) (n : nat) : nat :=
match n with
| O => f O
| S m => f (S m) + sum_of f m
end.
Lemma sum_of_pow : forall n,
S (sum_of (NPeano.pow 2) n) = NPeano.pow 2 (S n).
intro n; induction n.
- reflexivity.
- simpl sum_of ; rewrite plus_n_Sm, IHn.
simpl ; repeat rewrite <- plus_n_O ; reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment