Require Import Inclusion. Require Import ZArith. Require Import Zwf. Require Import Omega. Open Scope Z_scope. Lemma half_wf : well_founded (fun i j : Z => 0 < i /\ j = 2* i). Proof. apply wf_incl with (Zwf 0). intros i j [H H0];split;auto with zarith. apply Zwf_well_founded. Qed.