theory Pr
imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"
begin

lemma 
  fixes a b::nat
  shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"
apply(simp add: power2_sum)
done

lemma
  fixes a b c::"real"
  assumes eq: "a * c \<le> b * c" and ineq: "b < a"
  shows "c \<le> 0"
proof -
  {
    assume  "0 < c" 
    then have "b * c < a * c" using ineq by(auto)
    then have "False" using eq by auto
  } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) 
qed
    



lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"
by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))



lemma 
 fixes n::"nat"
 assumes a: "n > 1"
    and  b: "\<not>(prime n)"
 shows "\<not>(prime ((2 ^ n) - 1))"   
using a b
apply(induct n)
apply(simp)
apply(simp)



end