Skip to content

Instantly share code, notes, and snippets.

@palmskog

palmskog/gist:3f9f919efb34ebd59a977e6b357771a3

Created December 15, 2016 21:57
Show Gist options
  • Save palmskog/3f9f919efb34ebd59a977e6b357771a3 to your computer and use it in GitHub Desktop.
Save palmskog/3f9f919efb34ebd59a977e6b357771a3 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
Lemma lt_2xp1 : forall x i : nat, i < x -> 1 + 2 * i < x + x.
Proof.
Admitted.
Lemma lt_2xp : forall x i : nat, i < x -> 2 * i < x + x.
Proof.
Admitted.
Lemma lt_div2_2pow : forall n' m,  m < 2 ^ (S n') -> Nat.div2 m < 2 ^ n'.
Proof.
Admitted.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment