src/HOL/Library/Poly_Mapping.thy

    "(\<And>x. x \<in> Poly_Mapping.keys c \<Longrightarrow> f x = 0) \<Longrightarrow> frag_extend f c = 0"
   by (simp add: frag_extend_def)
 
 lemma keys_frag_extend: "Poly_Mapping.keys(frag_extend f c) \<subseteq> (\<Union>x \<in> Poly_Mapping.keys c. Poly_Mapping.keys(f x))"
   unfolding frag_extend_def
-  by (smt SUP_mono' keys_cmul keys_sum order_trans)
+  using keys_sum by fastforce
 
 lemma frag_expansion: "a = frag_extend frag_of a"
 proof -
   have *: "finite I
         \<Longrightarrow> Poly_Mapping.lookup (\<Sum>i\<in>I. frag_cmul (Poly_Mapping.lookup a i) (frag_of i)) j =