equal
deleted
inserted
replaced
44 |
44 |
45 lemma pq_coprime: "coprime p q" |
45 lemma pq_coprime: "coprime p q" |
46 using pq_neq p_prime primes_coprime_nat q_prime by blast |
46 using pq_neq p_prime primes_coprime_nat q_prime by blast |
47 |
47 |
48 lemma pq_coprime_int: "coprime (int p) (int q)" |
48 lemma pq_coprime_int: "coprime (int p) (int q)" |
49 using pq_coprime transfer_int_nat_gcd(1) by presburger |
49 by (simp add: gcd_int_def pq_coprime) |
50 |
50 |
51 lemma qp_ineq: "int p * k \<le> (int p * int q - 1) div 2 \<longleftrightarrow> k \<le> (int q - 1) div 2" |
51 lemma qp_ineq: "int p * k \<le> (int p * int q - 1) div 2 \<longleftrightarrow> k \<le> (int q - 1) div 2" |
52 proof - |
52 proof - |
53 have "2 * int p * k \<le> int p * int q - 1 \<longleftrightarrow> 2 * k \<le> int q - 1" |
53 have "2 * int p * k \<le> int p * int q - 1 \<longleftrightarrow> 2 * k \<le> int q - 1" |
54 using p_ge_0 by auto |
54 using p_ge_0 by auto |