# Library Stdlib.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

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|

Let f (z:Z) := Z.abs_nat (z - c).

Lemma Zwf_well_founded : well_founded (Zwf c).

End wf_proof.

#[global]

Hint Resolve Zwf_well_founded: datatypes.

We also define the other family of relations:
x (Zwf_up c) y iff 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|

Let f (z:Z) := Z.abs_nat (c - z).

Lemma Zwf_up_well_founded : well_founded (Zwf_up c).

End wf_proof_up.

#[global]

Hint Resolve Zwf_up_well_founded: datatypes.