Skip to content

Instantly share code, notes, and snippets.

@pasberth

pasberth/a.v

Created October 20, 2014 02:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pasberth/e3acfdf6e1e510ffa0cd to your computer and use it in GitHub Desktop.
Save pasberth/e3acfdf6e1e510ffa0cd to your computer and use it in GitHub Desktop.
Download ZIP
Raw
a.v
Require Import Arith.
Goal forall n : nat, S (n + n + n * n) = S (n + n * S n).
Proof.
intro n.
rewrite <- mult_n_Sm.
rewrite <- plus_assoc.
rewrite (plus_comm n (n * n)).
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment