Skip to content

Instantly share code, notes, and snippets.

@takeouchida

takeouchida/div2_double.v

Created March 26, 2012 15:19
Show Gist options
  • Save takeouchida/2205840 to your computer and use it in GitHub Desktop.
Save takeouchida/2205840 to your computer and use it in GitHub Desktop.
Download ZIP
x * 2 / 2 = x
Raw
div2_double.v
Require Import Div2.
Theorem div2_double : forall x, div2 (double x) = x.
intro x.
induction x.
reflexivity.
unfold double.
unfold double in IHx.
rewrite plus_Sn_m.
rewrite Plus.plus_comm.
rewrite plus_Sn_m.
simpl.
rewrite IHx.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment