proposition: Fact lc_length_perm l m : l ⪼ m -> ⌊m⌋ < ⌊l⌋ \/ l ~p m.
proof: Proof. induction 1 as [ | ? ? ? ? [] | | | ? ? ? ? [] ? [] ]; simpl; eauto; repeat match goal with | H: _ ⪼ _ |- _ => apply lc_length in H end; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)