Skip to content

Instantly share code, notes, and snippets.

@KeenS

KeenS/2-9.v

Created April 13, 2014 16:38
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 KeenS/10591540 to your computer and use it in GitHub Desktop.
Save KeenS/10591540 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
2-9.v
Require Import Arith.
Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
intros.
rewrite (plus_assoc (n + m) p q).
rewrite (plus_assoc (n + p) m q).
rewrite <- (plus_assoc n m p).
rewrite <- (plus_assoc n p m).
rewrite (plus_comm m p).
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment