proposition: Fact prefix_app_lft l r1 r2 : r1 <p r2 -> l++r1 <p l++r2.
proof: Proof. intros (a & ?); subst. exists a; rewrite <- app_assoc; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)