proposition: Lemma well_founded_Dlt : well_founded Dlt.
proof: Proof. unfold Dlt. apply wf_incl with (R2 := (fun x y : D => Zwf 0 (val x) (val y))). unfold inclusion, Zwf. intros (x,Hx) (y,Hy). simpl. intuition lia. apply (wf_inverse_image D Z (Zwf 0) val). apply Zwf_well_founded. Qed.
imports: CoLoR(LogicUtil) Coq(Lia) CoLoR(RelUtil) Coq(Zwf Wellfounded)