Require Import ZArith. Require Import Wf. Require Import Inverse_Image. Require Import Inclusion. Require Import Zwf. Section Zmeasure_def. Variable A:Type. Variable m : A -> Z. Variable bt : Z. Local Open Scope Z_scope. Definition Zmeasure := fun a b => bt <= m a < m b. Theorem Zmeasure_wf : well_founded Zmeasure. Proof. unfold Zmeasure. generalize (wf_inverse_image _ _ (Zwf bt) m (Zwf_well_founded bt)). unfold Zwf;intro. eapply wf_incl. 2:eexact H. red;intros x y [H0 H1]; omega. Qed. End Zmeasure_def. Implicit Arguments Zmeasure [A].