proposition: Lemma Rwf : well_founded R.
proof: Proof. eapply wf_incl. 2: eapply wf_inverse_image with (f:= fun q => p - q). 2: apply lt_wf. intros q q'; unfold R; lia. Defined.
imports: Coq(Arith Lia Inclusion Inverse_Image) hydras(DecPreOrder)