Skip to content

Instantly share code, notes, and snippets.

@KeenS
Created April 13, 2014 16:00
Show Gist options
  • Save KeenS/10589974 to your computer and use it in GitHub Desktop.
Save KeenS/10589974 to your computer and use it in GitHub Desktop.
Require Import Arith.
Goal forall x y, x < y -> x + 10 < y + 10.
Proof.
intros.
apply plus_lt_compat_r.
apply H.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment