proposition: Lemma lhd_lc l : lhd l -> exists m, l ⪼ m /\ ⌊m⌋ < ⌊l⌋.
proof: Proof. induction 1 as [ l x H | l x H (m & H1 & H2) ]. + apply in_split in H as (l1 & l2 & ->). exists (l1++x::l2); split; simpl; try lia. apply lc_trans with (x::x::l1++l2). * apply perm_lc, perm_skip, Permutation_sym, Permutation_cons_app; auto. * apply lc_trans with (1 := lc_cntr _ _), perm_lc, Permutation_cons_app; auto. + exists (x::m); split; simpl; auto; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)