Skip to content

Instantly share code, notes, and snippets.

@totem3

totem3/le_n_0_eq.v

Created November 19, 2014 04:02
Show Gist options
  • Save totem3/b32e718bc1059ad54242 to your computer and use it in GitHub Desktop.
Save totem3/b32e718bc1059ad54242 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
le_n_0_eq.v
Require Import Arith.
Require Import NOrder.
Lemma le_n_0_eq n : n <= 0 -> 0 = n .
intros.
symmetry.
induction n.
reflexivity.
apply False_ind.
apply (NPeano.Nat.nle_succ_0 n).
apply H.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment