Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Lemma q5 : forall n : nat, 2 * somme id n = n * (n + 1).
- intros.
- induction n.
- simpl.
- trivial.
- simpl.
- replace (somme id n + id (S n) + (somme id n + id (S n) + 0)) with (2*(somme id n) + 2*(S n)).
- rewrite IHn.
- ring.
- simpl.
- ring_simplify.
- rewrite IHn.
- simpl.
- ring.
- Qed.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
