src/HOL/Old_Number_Theory/Factorization.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 57983 6edc3529bb4e child 58889 5b7a9633cfa8 permissions -rw-r--r--
simpler proof
 wenzelm@38159 ` 1` ```(* Title: HOL/Old_Number_Theory/Factorization.thy ``` wenzelm@38159 ` 2` ``` Author: Thomas Marthedal Rasmussen ``` paulson@9944 ` 3` ``` Copyright 2000 University of Cambridge ``` wenzelm@11049 ` 4` ```*) ``` paulson@9944 ` 5` wenzelm@11049 ` 6` ```header {* Fundamental Theorem of Arithmetic (unique factorization into primes) *} ``` wenzelm@11049 ` 7` haftmann@27368 ` 8` ```theory Factorization ``` wenzelm@41413 ` 9` ```imports Primes "~~/src/HOL/Library/Permutation" ``` haftmann@27368 ` 10` ```begin ``` paulson@9944 ` 11` paulson@9944 ` 12` wenzelm@11049 ` 13` ```subsection {* Definitions *} ``` paulson@9944 ` 14` wenzelm@38159 ` 15` ```definition primel :: "nat list => bool" ``` wenzelm@38159 ` 16` ``` where "primel xs = (\p \ set xs. prime p)" ``` wenzelm@19670 ` 17` wenzelm@38159 ` 18` ```primrec nondec :: "nat list => bool" ``` wenzelm@38159 ` 19` ```where ``` wenzelm@11049 ` 20` ``` "nondec [] = True" ``` wenzelm@38159 ` 21` ```| "nondec (x # xs) = (case xs of [] => True | y # ys => x \ y \ nondec xs)" ``` paulson@9944 ` 22` wenzelm@38159 ` 23` ```primrec prod :: "nat list => nat" ``` wenzelm@38159 ` 24` ```where ``` wenzelm@11701 ` 25` ``` "prod [] = Suc 0" ``` wenzelm@38159 ` 26` ```| "prod (x # xs) = x * prod xs" ``` wenzelm@11049 ` 27` wenzelm@38159 ` 28` ```primrec oinsert :: "nat => nat list => nat list" ``` wenzelm@38159 ` 29` ```where ``` wenzelm@11049 ` 30` ``` "oinsert x [] = [x]" ``` wenzelm@38159 ` 31` ```| "oinsert x (y # ys) = (if x \ y then x # y # ys else y # oinsert x ys)" ``` paulson@9944 ` 32` wenzelm@38159 ` 33` ```primrec sort :: "nat list => nat list" ``` wenzelm@38159 ` 34` ```where ``` wenzelm@11049 ` 35` ``` "sort [] = []" ``` wenzelm@38159 ` 36` ```| "sort (x # xs) = oinsert x (sort xs)" ``` wenzelm@11049 ` 37` wenzelm@11049 ` 38` wenzelm@11049 ` 39` ```subsection {* Arithmetic *} ``` wenzelm@11049 ` 40` wenzelm@11701 ` 41` ```lemma one_less_m: "(m::nat) \ m * k ==> m \ Suc 0 ==> Suc 0 < m" ``` wenzelm@19670 ` 42` ``` apply (cases m) ``` wenzelm@11049 ` 43` ``` apply auto ``` wenzelm@11049 ` 44` ``` done ``` wenzelm@11049 ` 45` wenzelm@11701 ` 46` ```lemma one_less_k: "(m::nat) \ m * k ==> Suc 0 < m * k ==> Suc 0 < k" ``` wenzelm@19670 ` 47` ``` apply (cases k) ``` wenzelm@11049 ` 48` ``` apply auto ``` wenzelm@11049 ` 49` ``` done ``` wenzelm@11049 ` 50` wenzelm@11049 ` 51` ```lemma mult_left_cancel: "(0::nat) < k ==> k * n = k * m ==> n = m" ``` wenzelm@11049 ` 52` ``` apply auto ``` wenzelm@11049 ` 53` ``` done ``` wenzelm@11049 ` 54` wenzelm@11701 ` 55` ```lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = Suc 0" ``` wenzelm@19670 ` 56` ``` apply (cases n) ``` wenzelm@11049 ` 57` ``` apply auto ``` wenzelm@11049 ` 58` ``` done ``` wenzelm@11049 ` 59` wenzelm@11049 ` 60` ```lemma prod_mn_less_k: ``` wenzelm@11701 ` 61` ``` "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k" ``` wenzelm@11049 ` 62` ``` apply (induct m) ``` wenzelm@11049 ` 63` ``` apply auto ``` wenzelm@11049 ` 64` ``` done ``` wenzelm@11049 ` 65` wenzelm@11049 ` 66` wenzelm@11049 ` 67` ```subsection {* Prime list and product *} ``` wenzelm@11049 ` 68` wenzelm@11049 ` 69` ```lemma prod_append: "prod (xs @ ys) = prod xs * prod ys" ``` wenzelm@11049 ` 70` ``` apply (induct xs) ``` haftmann@57512 ` 71` ``` apply (simp_all add: mult.assoc) ``` wenzelm@11049 ` 72` ``` done ``` wenzelm@11049 ` 73` wenzelm@11049 ` 74` ```lemma prod_xy_prod: ``` wenzelm@11049 ` 75` ``` "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys" ``` wenzelm@11049 ` 76` ``` apply auto ``` wenzelm@11049 ` 77` ``` done ``` wenzelm@11049 ` 78` wenzelm@11049 ` 79` ```lemma primel_append: "primel (xs @ ys) = (primel xs \ primel ys)" ``` wenzelm@11049 ` 80` ``` apply (unfold primel_def) ``` wenzelm@11049 ` 81` ``` apply auto ``` wenzelm@11049 ` 82` ``` done ``` wenzelm@11049 ` 83` nipkow@16663 ` 84` ```lemma prime_primel: "prime n ==> primel [n] \ prod [n] = n" ``` wenzelm@11049 ` 85` ``` apply (unfold primel_def) ``` wenzelm@11049 ` 86` ``` apply auto ``` wenzelm@11049 ` 87` ``` done ``` wenzelm@11049 ` 88` nipkow@16663 ` 89` ```lemma prime_nd_one: "prime p ==> \ p dvd Suc 0" ``` wenzelm@11049 ` 90` ``` apply (unfold prime_def dvd_def) ``` wenzelm@11049 ` 91` ``` apply auto ``` wenzelm@11049 ` 92` ``` done ``` wenzelm@11049 ` 93` paulson@23814 ` 94` ```lemma hd_dvd_prod: "prod (x # xs) = prod ys ==> x dvd (prod ys)" ``` paulson@23814 ` 95` ``` by (metis dvd_mult_left dvd_refl prod.simps(2)) ``` wenzelm@11049 ` 96` wenzelm@11049 ` 97` ```lemma primel_tl: "primel (x # xs) ==> primel xs" ``` wenzelm@11049 ` 98` ``` apply (unfold primel_def) ``` wenzelm@11049 ` 99` ``` apply auto ``` wenzelm@11049 ` 100` ``` done ``` wenzelm@11049 ` 101` nipkow@16663 ` 102` ```lemma primel_hd_tl: "(primel (x # xs)) = (prime x \ primel xs)" ``` wenzelm@11049 ` 103` ``` apply (unfold primel_def) ``` wenzelm@11049 ` 104` ``` apply auto ``` wenzelm@11049 ` 105` ``` done ``` wenzelm@11049 ` 106` nipkow@16663 ` 107` ```lemma primes_eq: "prime p ==> prime q ==> p dvd q ==> p = q" ``` wenzelm@11049 ` 108` ``` apply (unfold prime_def) ``` wenzelm@11049 ` 109` ``` apply auto ``` wenzelm@11049 ` 110` ``` done ``` wenzelm@11049 ` 111` wenzelm@11701 ` 112` ```lemma primel_one_empty: "primel xs ==> prod xs = Suc 0 ==> xs = []" ``` wenzelm@19670 ` 113` ``` apply (cases xs) ``` wenzelm@19670 ` 114` ``` apply (simp_all add: primel_def prime_def) ``` wenzelm@11049 ` 115` ``` done ``` wenzelm@11049 ` 116` nipkow@16663 ` 117` ```lemma prime_g_one: "prime p ==> Suc 0 < p" ``` wenzelm@11049 ` 118` ``` apply (unfold prime_def) ``` wenzelm@11049 ` 119` ``` apply auto ``` wenzelm@11049 ` 120` ``` done ``` wenzelm@11049 ` 121` nipkow@16663 ` 122` ```lemma prime_g_zero: "prime p ==> 0 < p" ``` wenzelm@11049 ` 123` ``` apply (unfold prime_def) ``` wenzelm@11049 ` 124` ``` apply auto ``` wenzelm@11049 ` 125` ``` done ``` wenzelm@11049 ` 126` wenzelm@19670 ` 127` ```lemma primel_nempty_g_one: ``` wenzelm@19670 ` 128` ``` "primel xs \ xs \ [] \ Suc 0 < prod xs" ``` wenzelm@11049 ` 129` ``` apply (induct xs) ``` wenzelm@19670 ` 130` ``` apply simp ``` nipkow@44890 ` 131` ``` apply (fastforce simp: primel_def prime_def elim: one_less_mult) ``` wenzelm@11049 ` 132` ``` done ``` wenzelm@11049 ` 133` wenzelm@11049 ` 134` ```lemma primel_prod_gz: "primel xs ==> 0 < prod xs" ``` wenzelm@11049 ` 135` ``` apply (induct xs) ``` wenzelm@19670 ` 136` ``` apply (auto simp: primel_def prime_def) ``` wenzelm@11049 ` 137` ``` done ``` wenzelm@11049 ` 138` wenzelm@11049 ` 139` wenzelm@11049 ` 140` ```subsection {* Sorting *} ``` wenzelm@11049 ` 141` wenzelm@19670 ` 142` ```lemma nondec_oinsert: "nondec xs \ nondec (oinsert x xs)" ``` wenzelm@11049 ` 143` ``` apply (induct xs) ``` wenzelm@19670 ` 144` ``` apply simp ``` wenzelm@19670 ` 145` ``` apply (case_tac xs) ``` blanchet@57983 ` 146` ``` apply (simp_all cong del: list.case_cong_weak) ``` wenzelm@11049 ` 147` ``` done ``` wenzelm@11049 ` 148` wenzelm@11049 ` 149` ```lemma nondec_sort: "nondec (sort xs)" ``` wenzelm@11049 ` 150` ``` apply (induct xs) ``` wenzelm@11049 ` 151` ``` apply simp_all ``` wenzelm@11049 ` 152` ``` apply (erule nondec_oinsert) ``` wenzelm@11049 ` 153` ``` done ``` wenzelm@11049 ` 154` wenzelm@11049 ` 155` ```lemma x_less_y_oinsert: "x \ y ==> l = y # ys ==> x # l = oinsert x l" ``` wenzelm@11049 ` 156` ``` apply simp_all ``` wenzelm@11049 ` 157` ``` done ``` wenzelm@11049 ` 158` wenzelm@19670 ` 159` ```lemma nondec_sort_eq [rule_format]: "nondec xs \ xs = sort xs" ``` wenzelm@11049 ` 160` ``` apply (induct xs) ``` wenzelm@11049 ` 161` ``` apply safe ``` wenzelm@11049 ` 162` ``` apply simp_all ``` nipkow@15236 ` 163` ``` apply (case_tac xs) ``` wenzelm@11049 ` 164` ``` apply simp_all ``` nipkow@15236 ` 165` ``` apply (case_tac xs) ``` wenzelm@11049 ` 166` ``` apply simp ``` nipkow@15236 ` 167` ``` apply (rule_tac y = aa and ys = list in x_less_y_oinsert) ``` wenzelm@11049 ` 168` ``` apply simp_all ``` wenzelm@11049 ` 169` ``` done ``` wenzelm@11049 ` 170` wenzelm@11049 ` 171` ```lemma oinsert_x_y: "oinsert x (oinsert y l) = oinsert y (oinsert x l)" ``` wenzelm@11049 ` 172` ``` apply (induct l) ``` wenzelm@11049 ` 173` ``` apply auto ``` wenzelm@11049 ` 174` ``` done ``` wenzelm@11049 ` 175` wenzelm@11049 ` 176` wenzelm@11049 ` 177` ```subsection {* Permutation *} ``` wenzelm@11049 ` 178` wenzelm@11049 ` 179` ```lemma perm_primel [rule_format]: "xs <~~> ys ==> primel xs --> primel ys" ``` wenzelm@11049 ` 180` ``` apply (unfold primel_def) ``` wenzelm@19670 ` 181` ``` apply (induct set: perm) ``` nipkow@16663 ` 182` ``` apply simp ``` nipkow@16663 ` 183` ``` apply simp ``` nipkow@16663 ` 184` ``` apply (simp (no_asm)) ``` nipkow@16663 ` 185` ``` apply blast ``` nipkow@16663 ` 186` ``` apply blast ``` wenzelm@11049 ` 187` ``` done ``` wenzelm@11049 ` 188` wenzelm@19670 ` 189` ```lemma perm_prod: "xs <~~> ys ==> prod xs = prod ys" ``` wenzelm@19670 ` 190` ``` apply (induct set: perm) ``` haftmann@57514 ` 191` ``` apply (simp_all add: ac_simps) ``` wenzelm@11049 ` 192` ``` done ``` paulson@9944 ` 193` wenzelm@11049 ` 194` ```lemma perm_subst_oinsert: "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys" ``` wenzelm@19670 ` 195` ``` apply (induct set: perm) ``` wenzelm@11049 ` 196` ``` apply auto ``` wenzelm@11049 ` 197` ``` done ``` wenzelm@11049 ` 198` wenzelm@11049 ` 199` ```lemma perm_oinsert: "x # xs <~~> oinsert x xs" ``` wenzelm@11049 ` 200` ``` apply (induct xs) ``` wenzelm@11049 ` 201` ``` apply auto ``` wenzelm@11049 ` 202` ``` done ``` wenzelm@11049 ` 203` wenzelm@11049 ` 204` ```lemma perm_sort: "xs <~~> sort xs" ``` wenzelm@11049 ` 205` ``` apply (induct xs) ``` wenzelm@11049 ` 206` ``` apply (auto intro: perm_oinsert elim: perm_subst_oinsert) ``` wenzelm@11049 ` 207` ``` done ``` wenzelm@11049 ` 208` wenzelm@11049 ` 209` ```lemma perm_sort_eq: "xs <~~> ys ==> sort xs = sort ys" ``` wenzelm@19670 ` 210` ``` apply (induct set: perm) ``` wenzelm@11049 ` 211` ``` apply (simp_all add: oinsert_x_y) ``` wenzelm@11049 ` 212` ``` done ``` wenzelm@11049 ` 213` wenzelm@11049 ` 214` wenzelm@11049 ` 215` ```subsection {* Existence *} ``` wenzelm@11049 ` 216` wenzelm@11049 ` 217` ```lemma ex_nondec_lemma: ``` wenzelm@11049 ` 218` ``` "primel xs ==> \ys. primel ys \ nondec ys \ prod ys = prod xs" ``` wenzelm@11049 ` 219` ``` apply (blast intro: nondec_sort perm_prod perm_primel perm_sort perm_sym) ``` wenzelm@11049 ` 220` ``` done ``` wenzelm@11049 ` 221` wenzelm@11049 ` 222` ```lemma not_prime_ex_mk: ``` nipkow@16663 ` 223` ``` "Suc 0 < n \ \ prime n ==> ``` wenzelm@11701 ` 224` ``` \m k. Suc 0 < m \ Suc 0 < k \ m < n \ k < n \ n = m * k" ``` wenzelm@11049 ` 225` ``` apply (unfold prime_def dvd_def) ``` wenzelm@11049 ` 226` ``` apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k) ``` wenzelm@11049 ` 227` ``` done ``` wenzelm@11049 ` 228` wenzelm@11049 ` 229` ```lemma split_primel: ``` wenzelm@25687 ` 230` ``` "primel xs \ primel ys \ \l. primel l \ prod l = prod xs * prod ys" ``` wenzelm@25687 ` 231` ``` apply (rule exI) ``` wenzelm@25687 ` 232` ``` apply safe ``` wenzelm@25687 ` 233` ``` apply (rule_tac [2] prod_append) ``` wenzelm@25687 ` 234` ``` apply (simp add: primel_append) ``` wenzelm@25687 ` 235` ``` done ``` wenzelm@11049 ` 236` wenzelm@11701 ` 237` ```lemma factor_exists [rule_format]: "Suc 0 < n --> (\l. primel l \ prod l = n)" ``` wenzelm@11049 ` 238` ``` apply (induct n rule: nat_less_induct) ``` wenzelm@11049 ` 239` ``` apply (rule impI) ``` nipkow@16663 ` 240` ``` apply (case_tac "prime n") ``` wenzelm@11049 ` 241` ``` apply (rule exI) ``` wenzelm@11049 ` 242` ``` apply (erule prime_primel) ``` wenzelm@11049 ` 243` ``` apply (cut_tac n = n in not_prime_ex_mk) ``` wenzelm@11049 ` 244` ``` apply (auto intro!: split_primel) ``` wenzelm@11049 ` 245` ``` done ``` wenzelm@11049 ` 246` wenzelm@11701 ` 247` ```lemma nondec_factor_exists: "Suc 0 < n ==> \l. primel l \ nondec l \ prod l = n" ``` wenzelm@11049 ` 248` ``` apply (erule factor_exists [THEN exE]) ``` wenzelm@11049 ` 249` ``` apply (blast intro!: ex_nondec_lemma) ``` wenzelm@11049 ` 250` ``` done ``` wenzelm@11049 ` 251` wenzelm@11049 ` 252` wenzelm@11049 ` 253` ```subsection {* Uniqueness *} ``` wenzelm@11049 ` 254` wenzelm@11049 ` 255` ```lemma prime_dvd_mult_list [rule_format]: ``` nipkow@16663 ` 256` ``` "prime p ==> p dvd (prod xs) --> (\m. m:set xs \ p dvd m)" ``` wenzelm@11049 ` 257` ``` apply (induct xs) ``` paulson@11364 ` 258` ``` apply (force simp add: prime_def) ``` paulson@11364 ` 259` ``` apply (force dest: prime_dvd_mult) ``` wenzelm@11049 ` 260` ``` done ``` wenzelm@11049 ` 261` wenzelm@11049 ` 262` ```lemma hd_xs_dvd_prod: ``` wenzelm@11049 ` 263` ``` "primel (x # xs) ==> primel ys ==> prod (x # xs) = prod ys ``` wenzelm@11049 ` 264` ``` ==> \m. m \ set ys \ x dvd m" ``` wenzelm@11049 ` 265` ``` apply (rule prime_dvd_mult_list) ``` wenzelm@11049 ` 266` ``` apply (simp add: primel_hd_tl) ``` wenzelm@11049 ` 267` ``` apply (erule hd_dvd_prod) ``` wenzelm@11049 ` 268` ``` done ``` wenzelm@11049 ` 269` wenzelm@11049 ` 270` ```lemma prime_dvd_eq: "primel (x # xs) ==> primel ys ==> m \ set ys ==> x dvd m ==> x = m" ``` wenzelm@11049 ` 271` ``` apply (rule primes_eq) ``` wenzelm@11049 ` 272` ``` apply (auto simp add: primel_def primel_hd_tl) ``` wenzelm@11049 ` 273` ``` done ``` paulson@9944 ` 274` wenzelm@11049 ` 275` ```lemma hd_xs_eq_prod: ``` wenzelm@11049 ` 276` ``` "primel (x # xs) ==> ``` wenzelm@11049 ` 277` ``` primel ys ==> prod (x # xs) = prod ys ==> x \ set ys" ``` wenzelm@11049 ` 278` ``` apply (frule hd_xs_dvd_prod) ``` wenzelm@11049 ` 279` ``` apply auto ``` wenzelm@11049 ` 280` ``` apply (drule prime_dvd_eq) ``` wenzelm@11049 ` 281` ``` apply auto ``` wenzelm@11049 ` 282` ``` done ``` wenzelm@11049 ` 283` wenzelm@11049 ` 284` ```lemma perm_primel_ex: ``` wenzelm@11049 ` 285` ``` "primel (x # xs) ==> ``` wenzelm@11049 ` 286` ``` primel ys ==> prod (x # xs) = prod ys ==> \l. ys <~~> (x # l)" ``` wenzelm@11049 ` 287` ``` apply (rule exI) ``` wenzelm@11049 ` 288` ``` apply (rule perm_remove) ``` wenzelm@11049 ` 289` ``` apply (erule hd_xs_eq_prod) ``` wenzelm@11049 ` 290` ``` apply simp_all ``` wenzelm@11049 ` 291` ``` done ``` wenzelm@11049 ` 292` wenzelm@11049 ` 293` ```lemma primel_prod_less: ``` wenzelm@11049 ` 294` ``` "primel (x # xs) ==> ``` wenzelm@11049 ` 295` ``` primel ys ==> prod (x # xs) = prod ys ==> prod xs < prod ys" ``` wenzelm@26316 ` 296` ``` by (metis less_asym linorder_neqE_nat mult_less_cancel2 nat_0_less_mult_iff ``` wenzelm@25180 ` 297` ``` nat_less_le nat_mult_1 prime_def primel_hd_tl primel_prod_gz prod.simps(2)) ``` wenzelm@11049 ` 298` wenzelm@11049 ` 299` ```lemma prod_one_empty: ``` nipkow@16663 ` 300` ``` "primel xs ==> p * prod xs = p ==> prime p ==> xs = []" ``` wenzelm@11049 ` 301` ``` apply (auto intro: primel_one_empty simp add: prime_def) ``` wenzelm@11049 ` 302` ``` done ``` wenzelm@11049 ` 303` wenzelm@11049 ` 304` ```lemma uniq_ex_aux: ``` wenzelm@11049 ` 305` ``` "\m. m < prod ys --> (\xs ys. primel xs \ primel ys \ ``` wenzelm@11049 ` 306` ``` prod xs = prod ys \ prod xs = m --> xs <~~> ys) ==> ``` wenzelm@11049 ` 307` ``` primel list ==> primel x ==> prod list = prod x ==> prod x < prod ys ``` wenzelm@11049 ` 308` ``` ==> x <~~> list" ``` wenzelm@11049 ` 309` ``` apply simp ``` wenzelm@11049 ` 310` ``` done ``` paulson@9944 ` 311` wenzelm@11049 ` 312` ```lemma factor_unique [rule_format]: ``` wenzelm@11049 ` 313` ``` "\xs ys. primel xs \ primel ys \ prod xs = prod ys \ prod xs = n ``` wenzelm@11049 ` 314` ``` --> xs <~~> ys" ``` wenzelm@11049 ` 315` ``` apply (induct n rule: nat_less_induct) ``` wenzelm@11049 ` 316` ``` apply safe ``` wenzelm@11049 ` 317` ``` apply (case_tac xs) ``` wenzelm@11049 ` 318` ``` apply (force intro: primel_one_empty) ``` wenzelm@11049 ` 319` ``` apply (rule perm_primel_ex [THEN exE]) ``` wenzelm@11049 ` 320` ``` apply simp_all ``` wenzelm@11049 ` 321` ``` apply (rule perm.trans [THEN perm_sym]) ``` wenzelm@11049 ` 322` ``` apply assumption ``` wenzelm@11049 ` 323` ``` apply (rule perm.Cons) ``` wenzelm@11049 ` 324` ``` apply (case_tac "x = []") ``` paulson@25493 ` 325` ``` apply (metis perm_prod perm_refl prime_primel primel_hd_tl primel_tl prod_one_empty) ``` paulson@25493 ` 326` ``` apply (metis nat_0_less_mult_iff nat_mult_eq_cancel1 perm_primel perm_prod primel_prod_gz primel_prod_less primel_tl prod.simps(2)) ``` wenzelm@11049 ` 327` ``` done ``` wenzelm@11049 ` 328` wenzelm@11049 ` 329` ```lemma perm_nondec_unique: ``` wenzelm@11049 ` 330` ``` "xs <~~> ys ==> nondec xs ==> nondec ys ==> xs = ys" ``` paulson@23814 ` 331` ``` by (metis nondec_sort_eq perm_sort_eq) ``` paulson@23814 ` 332` paulson@25493 ` 333` ```theorem unique_prime_factorization [rule_format]: ``` wenzelm@11701 ` 334` ``` "\n. Suc 0 < n --> (\!l. primel l \ nondec l \ prod l = n)" ``` paulson@25493 ` 335` ``` by (metis factor_unique nondec_factor_exists perm_nondec_unique) ``` wenzelm@11049 ` 336` wenzelm@11049 ` 337` ```end ```