Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
You can’t perform that action at this time.