proposition: Lemma lt_wf (a:A) : well_founded (@lt a).
proof: Proof. intro x; unfold lt; apply Acc_inverse_image. destruct x; cbn; apply ON_wf. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)