proposition: Lemma lhd_lseq l : lhd l -> exists m, l ≡ m /\ ⌊m⌋ < ⌊l⌋.
proof: Proof. intro H; apply lhd_lc in H as (? & ? & ?); eauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)