Library Coq.Wellfounded.Transitive_Closure
Author: Bruno Barras
Require
Import
Relation_Definitions
.
Require
Import
Relation_Operators
.
Section
Wf_Transitive_Closure
.
Variable
A
:
Type
.
Variable
R
:
relation
A
.
Notation
trans_clos
:= (
clos_trans
A
R
).
Lemma
incl_clos_trans
:
inclusion
A
R
trans_clos
.
Lemma
Acc_clos_trans
:
forall
x
:
A
,
Acc
R
x
->
Acc
trans_clos
x
.
Hint Resolve
Acc_clos_trans
.
Lemma
Acc_inv_trans
:
forall
x
y
:
A
,
trans_clos
y
x
->
Acc
R
x
->
Acc
R
y
.
Theorem
wf_clos_trans
:
well_founded
R
->
well_founded
trans_clos
.
End
Wf_Transitive_Closure
.