Skip to content

Instantly share code, notes, and snippets.

@co-dan

co-dan/nat_well_founded.v

Created January 16, 2015 14:25
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 co-dan/79f4f67b3f9566a1eb58 to your computer and use it in GitHub Desktop.
Save co-dan/79f4f67b3f9566a1eb58 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
nat_well_founded.v
Require Import Rel.
Require Import Coq.Init.Wf.
Theorem nat_wo: well_founded lt.
Proof.
intro n.
assert (forall y x, x < y -> Acc lt x) as A.
induction y.
+ intros x H; inversion H.
+ intros x H'. apply Acc_intro.
intros. apply IHy.
unfold lt. unfold lt in H,H'.
apply le_trans with (b:=x). assumption.
SearchAbout le.
apply le_S_n. assumption.
+ apply Acc_intro. apply A.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment