proposition: Fact list_has_dup_app_right l m : list_has_dup l -> list_has_dup (l++m).
proof: Proof. induction 1; simpl. + constructor 1; apply in_or_app; left; auto. + constructor 2; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)