# How many integers are in the solution set of $|x-2|\\leq5.6$ ? Show that it is 11.
# cases = [
# """
# theorem mathd_algebra_170:
# shows "card { n::int. abs (n - 2) \<le> 5 + 6 / 10} = 11"

# theorem
# fixes x :: real
# assumes h0 : "abs (x - 2) \<le> 5.6"
# shows "card {x::int. real_of_int x \<ge> -3.6 \<and> real_of_int x \<le> 7.6} = 11"
# """
# ]

cases =[
"""
theorem
fixes n :: nat
shows  "3 dvd (2^(2 * n + 1) + 1)"


theorem
fixes n ::nat
shows "(3::nat) dvd (2^(2 * n + 1) + 1)"
"""
]
# 2 subgoals




cases = [
"""
theorem
fixes n :: nat
shows  "2 dvd (4^n)"
 

theorem
fixes n :: nat
shows  "2 dvd (4 ^ n)"
 
"""
]

# cases = [
# """
# theorem
# fixes num_girls :: nat
# assumes h0 : "num_girls mod 8 = 7"
# shows  "num_girls mod 4 = 3"


# theorem
# fixes n :: nat
# assumes h0 : "n mod 8 = (7::nat)"
# shows "n mod 4 = 3"
# """
# ]

# cases=[
# """
# theorem
# fixes n :: nat
# shows  "gcd (21 * n + 4) (14 * n + 3) = 1"


# theorem
# fixes n :: nat
# shows  "gcd (21*n + 4) (14*n + 3) = 1"
# """
# ]

cases = [
    """
theorem\nfixes a b :: real\nassumes h0 : \"log 8 a + log 4 (b powr 2) = 5\"\nand h1 : \"log 8 b + log 4 (a powr 2) = 7\"\nshows  \"a * b = 512\"


theorem\nfixes a b ::real\nassumes \"(ln a) / (ln 8) + (ln (b^2)) / (ln 4) = 5\"\n\"(ln b) / (ln 8) + (ln (a^2)) / (ln 4) = 7\"\nshows \"a * b = 512\"
"""
]

cases = [
    """
theorem\nfixes a b :: real\nassumes h0 : \"log 8 a + log 4 (b^2) = 5\"\nand h1 : \"log 8 b + log 4 (a^2) = 7\"\nshows  \"a * b = 512\"


theorem\nfixes a b :: real\nassumes h0 : \"log 8 a + log 4 (b powr 2) = 5\"\nand h1 : \"log 8 b + log 4 (a powr 2) = 7\"\nshows  \"a * b = 512\"
"""
]

cases=[
"""
theorem
fixes f :: "nat \<Rightarrow> nat"
assumes h0 : "\<forall> n > 0. f (n + 1) > f (f n)"
shows  "f n = n"


theorem
fixes f :: "nat \<Rightarrow> nat"
assumes "\<forall> n. f (f n) < f (n + 1)"
and "\<forall> n. f n >0"
shows "\<forall> n. f n = n"
"""
]

cases=[
"""
theorem
fixes f :: "real \<Rightarrow> real"
assumes h0 : "bij f"
and h1 : "f 2 = 4"
and h2 : "f (inv f 2) = 4"
shows "f (f 2) = 2"


theorem
fixes x :: real and f :: "real \<Rightarrow> real"
assumes h0 : "bij f"
and h1 : "f 2 = 4"
and h2 : "(inv f) 2 = 4"
shows "f (f 2) = 2"
"""
]

cases=[
"""
theorem
fixes x y :: real
assumes "x = 0.66"
and "y = 6"
shows "x * y = 4"


theorem
fixes a b :: real
assumes "a = 2/3"
and "b = 6"
shows "a * b = 4"
"""
]

cases=["""
theorem
fixes x :: real
assumes h0 : "3 * x - 1 \<noteq> 0"
and h1 : "x + 1 \<noteq> 0"
and h2 : "1 / (3 * x - 1) = 2 / (x + 1)"
shows "x = 3 / 5"


theorem
fixes x :: real
assumes h0 : "(1 / (3 * x - 1)) = (2 / (x + 1))"
shows "x = 3 / 5"
"""]