proposition: Fact lc_length l m : l ⪼ m -> ⌊m⌋ <= ⌊l⌋.
proof: Proof. induction 1; simpl; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)