Library Coq.ZArith.Zwf
Well-founded relations on Z.
We define the following family of relations on Z x Z:
x (Zwf c) y iff x < y & c <= y
Definition Zwf (
c x y:Z) :=
c <=
y /\
x <
y.
and we prove that (Zwf c) is well founded
The proof of well-foundness is classic: we do the proof by induction
on a measure in nat, which is here |x-c|
n= 0
inductive case
We also define the other family of relations:
x (Zwf_up c) y iff y < x <= c
Definition Zwf_up (
c x y:Z) :=
y <
x <=
c.
and we prove that (Zwf_up c) is well founded
The proof of well-foundness is classic: we do the proof by induction
on a measure in nat, which is here |c-x|