equal
deleted
inserted
replaced
656 from assms have "n = prod_mset (prime_factorization n)" |
656 from assms have "n = prod_mset (prime_factorization n)" |
657 by (simp add: prod_mset_prime_factorization) |
657 by (simp add: prod_mset_prime_factorization) |
658 also have "\<dots> = prod_mset (mset xs)" by (simp add: xs) |
658 also have "\<dots> = prod_mset (mset xs)" by (simp add: xs) |
659 also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all |
659 also have "\<dots> = foldr op * xs 1" by (induction xs) simp_all |
660 finally have "foldr op * xs 1 = n" .. |
660 finally have "foldr op * xs 1 = n" .. |
661 moreover have "\<forall>p\<in>#mset xs. prime p" |
661 moreover from xs have "\<forall>p\<in>#mset xs. prime p" |
662 by (subst xs) (auto dest: in_prime_factorization_imp_prime) |
662 by auto |
663 ultimately have "primefact xs n" by (auto simp: primefact_def) |
663 ultimately have "primefact xs n" by (auto simp: primefact_def) |
664 thus ?thesis .. |
664 thus ?thesis .. |
665 qed |
665 qed |
666 |
666 |
667 lemma primefact_contains: |
667 lemma primefact_contains: |