equal
deleted
inserted
replaced
13 "~~/src/HOL/Library/Code_Target_Numeral" |
13 "~~/src/HOL/Library/Code_Target_Numeral" |
14 begin |
14 begin |
15 |
15 |
16 text {* |
16 text {* |
17 A constructive version of the proof of Euclid's theorem by |
17 A constructive version of the proof of Euclid's theorem by |
18 Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. |
18 Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. |
19 *} |
19 *} |
20 |
20 |
21 lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m" |
21 lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m" |
22 by (induct m) auto |
22 by (induct m) auto |
23 |
23 |