Structure gcdTheory

signature gcdTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val is_gcd_def : thm
    val lcm_def : thm
  
  (*  Theorems  *)
    val BINARY_GCD : thm
    val DIVIDES_EXP_BASE : thm
    val EUCLID_LEMMA : thm
    val FACTOR_OUT_GCD : thm
    val FACT_MOD_PRIME : thm
    val GCD_0 : thm
    val GCD_0L : thm
    val GCD_0R : thm
    val GCD_1 : thm
    val GCD_ADD_L : thm
    val GCD_ADD_L_THM : thm
    val GCD_ADD_R : thm
    val GCD_ADD_R_THM : thm
    val GCD_ASSOC : thm
    val GCD_ASSOC_COMM : thm
    val GCD_CANCEL_MULT : thm
    val GCD_COMM : thm
    val GCD_COMMON_FACTOR : thm
    val GCD_DIVIDES : thm
    val GCD_EFFICIENTLY : thm
    val GCD_EQ_0 : thm
    val GCD_EUCLID : thm
    val GCD_GCD : thm
    val GCD_IS_GCD : thm
    val GCD_IS_GREATEST_COMMON_DIVISOR : thm
    val GCD_LCM : thm
    val GCD_LINEAR : thm
    val GCD_MOD : thm
    val GCD_MOD_COMM : thm
    val GCD_MULTIPLE : thm
    val GCD_MULTIPLE_ALT : thm
    val GCD_ONE_PROPERTY : thm
    val GCD_POS : thm
    val GCD_PROPERTY : thm
    val GCD_REDUCE : thm
    val GCD_REDUCE_BY_COPRIME : thm
    val GCD_REF : thm
    val GCD_SUB_L : thm
    val GCD_SUB_R : thm
    val GCD_SUCfree_ind : thm
    val GCD_SYM : thm
    val IS_GCD_0L : thm
    val IS_GCD_0R : thm
    val IS_GCD_MINUS_L : thm
    val IS_GCD_MINUS_R : thm
    val IS_GCD_REF : thm
    val IS_GCD_SYM : thm
    val IS_GCD_UNIQUE : thm
    val LCM_0 : thm
    val LCM_1 : thm
    val LCM_ASSOC : thm
    val LCM_ASSOC_COMM : thm
    val LCM_COMM : thm
    val LCM_COMMON_COPRIME : thm
    val LCM_COMMON_FACTOR : thm
    val LCM_COPRIME : thm
    val LCM_DIVIDES : thm
    val LCM_DIVISORS : thm
    val LCM_EQ_0 : thm
    val LCM_IS_LCM : thm
    val LCM_IS_LEAST_COMMON_MULTIPLE : thm
    val LCM_LE : thm
    val LCM_LEAST : thm
    val LCM_POS : thm
    val LCM_PROPERTY : thm
    val LCM_REF : thm
    val LCM_SYM : thm
    val LINEAR_GCD : thm
    val L_EUCLIDES : thm
    val MOD_EQ : thm
    val MOD_EQ_DIFF : thm
    val MOD_MOD_EQN : thm
    val MOD_NONZERO_WHEN_GCD_ONE : thm
    val MOD_PLUS2 : thm
    val MOD_WITH_GCD_ONE : thm
    val PRIME_BIG_NOT_DIVIDES_FACT : thm
    val PRIME_GCD : thm
    val PRIME_IS_GCD : thm
    val PRODUCT_WITH_GCD_ONE : thm
    val P_EUCLIDES : thm
    val coprime_0 : thm
    val coprime_0L : thm
    val coprime_0R : thm
    val coprime_PRE : thm
    val coprime_SUC : thm
    val coprime_by_prime_factor : thm
    val coprime_by_prime_factor_le : thm
    val coprime_common_factor : thm
    val coprime_exp : thm
    val coprime_exp_comm : thm
    val coprime_factor_coprime : thm
    val coprime_factor_not_divides : thm
    val coprime_gt_1 : thm
    val coprime_mod : thm
    val coprime_mod_iff : thm
    val coprime_neq_1 : thm
    val coprime_prime_factor_coprime : thm
    val coprime_product_coprime : thm
    val coprime_product_coprime_iff : thm
    val coprime_product_coprime_sym : thm
    val coprime_product_divides : thm
    val coprime_sym : thm
    val divides_coprime_mul : thm
    val divides_iff_gcd_fix : thm
    val divides_iff_lcm_fix : thm
    val divides_imp_coprime_with_predecessor : thm
    val divides_imp_coprime_with_successor : thm
    val gcd_LESS_EQ : thm
    val gcd_compute : thm
    val gcd_coprime_cancel : thm
    val gcd_def : thm
    val gcd_ind : thm
    val prime_not_coprime_divides : thm
    val prime_not_divides_coprime : thm
    val primes_coprime : thm
(*
   [divides] Parent theory of "gcd"
   
   [is_gcd_def]  Definition
      
      ⊢ ∀a b c.
          is_gcd a b c ⇔
          c divides a ∧ c divides b ∧
          ∀d. d divides a ∧ d divides b ⇒ d divides c
   
   [lcm_def]  Definition
      
      ⊢ ∀m n. lcm m n = if m = 0 ∨ n = 0 then 0 else m * n DIV gcd m n
   
   [BINARY_GCD]  Theorem
      
      ⊢ ∀m n.
          (EVEN m ∧ EVEN n ⇒ gcd m n = 2 * gcd (m DIV 2) (n DIV 2)) ∧
          (EVEN m ∧ ODD n ⇒ gcd m n = gcd (m DIV 2) n)
   
   [DIVIDES_EXP_BASE]  Theorem
      
      ⊢ ∀a b n. prime a ∧ 0 < n ⇒ (a divides b ⇔ a divides b ** n)
   
   [EUCLID_LEMMA]  Theorem
      
      ⊢ ∀p x y. prime p ⇒ ((x * y) MOD p = 0 ⇔ x MOD p = 0 ∨ y MOD p = 0)
   
   [FACTOR_OUT_GCD]  Theorem
      
      ⊢ ∀n m.
          n ≠ 0 ∧ m ≠ 0 ⇒
          ∃p q. n = p * gcd n m ∧ m = q * gcd n m ∧ coprime p q
   
   [FACT_MOD_PRIME]  Theorem
      
      ⊢ ∀p n. prime p ∧ n < p ⇒ FACT n MOD p ≠ 0
   
   [GCD_0]  Theorem
      
      ⊢ ∀x. gcd 0 x = x ∧ gcd x 0 = x
   
   [GCD_0L]  Theorem
      
      ⊢ ∀a. gcd 0 a = a
   
   [GCD_0R]  Theorem
      
      ⊢ ∀a. gcd a 0 = a
   
   [GCD_1]  Theorem
      
      ⊢ coprime 1 x ∧ coprime x 1
   
   [GCD_ADD_L]  Theorem
      
      ⊢ ∀a b. gcd (a + b) a = gcd a b
   
   [GCD_ADD_L_THM]  Theorem
      
      ⊢ (∀a b. gcd (a + b) a = gcd a b) ∧ ∀a b. gcd (b + a) a = gcd a b
   
   [GCD_ADD_R]  Theorem
      
      ⊢ ∀a b. gcd a (a + b) = gcd a b
   
   [GCD_ADD_R_THM]  Theorem
      
      ⊢ (∀a b. gcd a (a + b) = gcd a b) ∧ ∀a b. gcd a (b + a) = gcd a b
   
   [GCD_ASSOC]  Theorem
      
      ⊢ ∀a b c. gcd a (gcd b c) = gcd (gcd a b) c
   
   [GCD_ASSOC_COMM]  Theorem
      
      ⊢ ∀a b c. gcd a (gcd b c) = gcd b (gcd a c)
   
   [GCD_CANCEL_MULT]  Theorem
      
      ⊢ ∀m n k. coprime m k ⇒ gcd m (k * n) = gcd m n
   
   [GCD_COMM]  Theorem
      
      ⊢ gcd a b = gcd b a
   
   [GCD_COMMON_FACTOR]  Theorem
      
      ⊢ ∀m n k. gcd (k * m) (k * n) = k * gcd m n
   
   [GCD_DIVIDES]  Theorem
      
      ⊢ ∀m n.
          0 < n ∧ 0 < m ⇒
          0 < gcd n m ∧ n MOD gcd n m = 0 ∧ m MOD gcd n m = 0
   
   [GCD_EFFICIENTLY]  Theorem
      
      ⊢ ∀a b. gcd a b = if a = 0 then b else gcd (b MOD a) a
   
   [GCD_EQ_0]  Theorem
      
      ⊢ ∀n m. gcd n m = 0 ⇔ n = 0 ∧ m = 0
   
   [GCD_EUCLID]  Theorem
      
      ⊢ ∀a b c. gcd a (b * a + c) = gcd a c
   
   [GCD_GCD]  Theorem
      
      ⊢ ∀m n. gcd n (gcd n m) = gcd n m
   
   [GCD_IS_GCD]  Theorem
      
      ⊢ ∀a b. is_gcd a b (gcd a b)
   
   [GCD_IS_GREATEST_COMMON_DIVISOR]  Theorem
      
      ⊢ ∀a b.
          gcd a b divides a ∧ gcd a b divides b ∧
          ∀d. d divides a ∧ d divides b ⇒ d divides gcd a b
   
   [GCD_LCM]  Theorem
      
      ⊢ ∀m n. gcd m n * lcm m n = m * n
   
   [GCD_LINEAR]  Theorem
      
      ⊢ ∀j k. 0 < j ⇒ ∃p q. p * j = q * k + gcd j k
   
   [GCD_MOD]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ gcd m n = gcd m (n MOD m)
   
   [GCD_MOD_COMM]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ gcd n m = gcd (n MOD m) m
   
   [GCD_MULTIPLE]  Theorem
      
      ⊢ ∀m n. 0 < n ∧ m MOD n = 0 ⇒ gcd m n = n
   
   [GCD_MULTIPLE_ALT]  Theorem
      
      ⊢ ∀m n. gcd (m * n) n = n
   
   [GCD_ONE_PROPERTY]  Theorem
      
      ⊢ ∀n x. 1 < n ∧ coprime n x ⇒ ∃k. (k * x) MOD n = 1 ∧ coprime n k
   
   [GCD_POS]  Theorem
      
      ⊢ ∀m n. 0 < m ∨ 0 < n ⇒ 0 < gcd m n
   
   [GCD_PROPERTY]  Theorem
      
      ⊢ ∀a b c.
          c = gcd a b ⇔
          c divides a ∧ c divides b ∧
          ∀x. x divides a ∧ x divides b ⇒ x divides c
   
   [GCD_REDUCE]  Theorem
      
      ⊢ ∀a b c. gcd (b * a + c) a = gcd a c
   
   [GCD_REDUCE_BY_COPRIME]  Theorem
      
      ⊢ ∀m n k. coprime m k ⇒ gcd m (k * n) = gcd m n
   
   [GCD_REF]  Theorem
      
      ⊢ ∀a. gcd a a = a
   
   [GCD_SUB_L]  Theorem
      
      ⊢ ∀a b. b ≤ a ⇒ gcd (a − b) b = gcd a b
   
   [GCD_SUB_R]  Theorem
      
      ⊢ ∀a b. a ≤ b ⇒ gcd a (b − a) = gcd a b
   
   [GCD_SUCfree_ind]  Theorem
      
      ⊢ ∀P. (∀y. P 0 y) ∧ (∀x y. P x y ⇒ P y x) ∧ (∀x. P x x) ∧
            (∀x y. 0 < x ∧ 0 < y ∧ P x y ⇒ P x (x + y)) ⇒
            ∀m n. P m n
   
   [GCD_SYM]  Theorem
      
      ⊢ ∀a b. gcd a b = gcd b a
   
   [IS_GCD_0L]  Theorem
      
      ⊢ ∀a. is_gcd 0 a a
   
   [IS_GCD_0R]  Theorem
      
      ⊢ ∀a. is_gcd a 0 a
   
   [IS_GCD_MINUS_L]  Theorem
      
      ⊢ ∀a b c. b ≤ a ∧ is_gcd (a − b) b c ⇒ is_gcd a b c
   
   [IS_GCD_MINUS_R]  Theorem
      
      ⊢ ∀a b c. a ≤ b ∧ is_gcd a (b − a) c ⇒ is_gcd a b c
   
   [IS_GCD_REF]  Theorem
      
      ⊢ ∀a. is_gcd a a a
   
   [IS_GCD_SYM]  Theorem
      
      ⊢ ∀a b c. is_gcd a b c ⇔ is_gcd b a c
   
   [IS_GCD_UNIQUE]  Theorem
      
      ⊢ ∀a b c d. is_gcd a b c ∧ is_gcd a b d ⇒ c = d
   
   [LCM_0]  Theorem
      
      ⊢ lcm 0 x = 0 ∧ lcm x 0 = 0
   
   [LCM_1]  Theorem
      
      ⊢ lcm 1 x = x ∧ lcm x 1 = x
   
   [LCM_ASSOC]  Theorem
      
      ⊢ ∀a b c. lcm a (lcm b c) = lcm (lcm a b) c
   
   [LCM_ASSOC_COMM]  Theorem
      
      ⊢ ∀a b c. lcm a (lcm b c) = lcm b (lcm a c)
   
   [LCM_COMM]  Theorem
      
      ⊢ lcm a b = lcm b a
   
   [LCM_COMMON_COPRIME]  Theorem
      
      ⊢ ∀a b. coprime a b ⇒ ∀c. lcm (a * c) (b * c) = a * b * c
   
   [LCM_COMMON_FACTOR]  Theorem
      
      ⊢ ∀m n k. lcm (k * m) (k * n) = k * lcm m n
   
   [LCM_COPRIME]  Theorem
      
      ⊢ ∀m n. coprime m n ⇒ lcm m n = m * n
   
   [LCM_DIVIDES]  Theorem
      
      ⊢ ∀n a b. a divides n ∧ b divides n ⇒ lcm a b divides n
   
   [LCM_DIVISORS]  Theorem
      
      ⊢ ∀m n. m divides lcm m n ∧ n divides lcm m n
   
   [LCM_EQ_0]  Theorem
      
      ⊢ ∀m n. lcm m n = 0 ⇔ m = 0 ∨ n = 0
   
   [LCM_IS_LCM]  Theorem
      
      ⊢ ∀m n p. m divides p ∧ n divides p ⇒ lcm m n divides p
   
   [LCM_IS_LEAST_COMMON_MULTIPLE]  Theorem
      
      ⊢ m divides lcm m n ∧ n divides lcm m n ∧
        ∀p. m divides p ∧ n divides p ⇒ lcm m n divides p
   
   [LCM_LE]  Theorem
      
      ⊢ 0 < m ∧ 0 < n ⇒ m ≤ lcm m n ∧ m ≤ lcm n m
   
   [LCM_LEAST]  Theorem
      
      ⊢ 0 < m ∧ 0 < n ⇒
        ∀p. 0 < p ∧ p < lcm m n ⇒ ¬(m divides p) ∨ ¬(n divides p)
   
   [LCM_POS]  Theorem
      
      ⊢ ∀m n. 0 < m ∧ 0 < n ⇒ 0 < lcm m n
   
   [LCM_PROPERTY]  Theorem
      
      ⊢ ∀a b c.
          c = lcm a b ⇔
          a divides c ∧ b divides c ∧
          ∀x. a divides x ∧ b divides x ⇒ c divides x
   
   [LCM_REF]  Theorem
      
      ⊢ ∀a. lcm a a = a
   
   [LCM_SYM]  Theorem
      
      ⊢ ∀a b. lcm a b = lcm b a
   
   [LINEAR_GCD]  Theorem
      
      ⊢ ∀n m. n ≠ 0 ⇒ ∃p q. p * n = q * m + gcd m n
   
   [L_EUCLIDES]  Theorem
      
      ⊢ ∀a b c. coprime a b ∧ b divides a * c ⇒ b divides c
   
   [MOD_EQ]  Theorem
      
      ⊢ ∀n a b. 0 < n ∧ b ≤ a ⇒ ((a − b) MOD n = 0 ⇔ a MOD n = b MOD n)
   
   [MOD_EQ_DIFF]  Theorem
      
      ⊢ ∀n a b. 0 < n ∧ a MOD n = b MOD n ⇒ (a − b) MOD n = 0
   
   [MOD_MOD_EQN]  Theorem
      
      ⊢ ∀n a b. 0 < n ∧ b ≤ a ⇒ (a MOD n = b MOD n ⇔ ∃c. a = b + c * n)
   
   [MOD_NONZERO_WHEN_GCD_ONE]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ ∀x. coprime n x ⇒ 0 < x ∧ 0 < x MOD n
   
   [MOD_PLUS2]  Theorem
      
      ⊢ ∀n x y. 0 < n ⇒ (x + y) MOD n = (x + y MOD n) MOD n
   
   [MOD_WITH_GCD_ONE]  Theorem
      
      ⊢ ∀n x. 0 < n ∧ coprime n x ⇒ coprime n (x MOD n)
   
   [PRIME_BIG_NOT_DIVIDES_FACT]  Theorem
      
      ⊢ ∀p k. prime p ∧ k < p ⇒ ¬(p divides FACT k)
   
   [PRIME_GCD]  Theorem
      
      ⊢ ∀p b. prime p ⇒ p divides b ∨ coprime p b
   
   [PRIME_IS_GCD]  Theorem
      
      ⊢ ∀p b. prime p ⇒ p divides b ∨ is_gcd p b 1
   
   [PRODUCT_WITH_GCD_ONE]  Theorem
      
      ⊢ ∀n x y. coprime n x ∧ coprime n y ⇒ coprime n (x * y)
   
   [P_EUCLIDES]  Theorem
      
      ⊢ ∀p a b. prime p ∧ p divides a * b ⇒ p divides a ∨ p divides b
   
   [coprime_0]  Theorem
      
      ⊢ ∀n. (coprime 0 n ⇔ n = 1) ∧ (coprime n 0 ⇔ n = 1)
   
   [coprime_0L]  Theorem
      
      ⊢ ∀n. coprime 0 n ⇔ n = 1
   
   [coprime_0R]  Theorem
      
      ⊢ ∀n. coprime n 0 ⇔ n = 1
   
   [coprime_PRE]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ coprime n (n − 1)
   
   [coprime_SUC]  Theorem
      
      ⊢ ∀n. coprime n (n + 1)
   
   [coprime_by_prime_factor]  Theorem
      
      ⊢ ∀m n. coprime m n ⇔ ∀p. prime p ⇒ ¬(p divides m ∧ p divides n)
   
   [coprime_by_prime_factor_le]  Theorem
      
      ⊢ ∀m n.
          0 < m ∧ 0 < n ⇒
          (coprime m n ⇔
           ∀p. prime p ∧ p ≤ m ∧ p ≤ n ⇒ ¬(p divides m ∧ p divides n))
   
   [coprime_common_factor]  Theorem
      
      ⊢ ∀a b c. coprime a b ∧ c divides a ∧ c divides b ⇒ c = 1
   
   [coprime_exp]  Theorem
      
      ⊢ ∀c m. coprime c m ⇒ ∀n. coprime (c ** n) m
   
   [coprime_exp_comm]  Theorem
      
      ⊢ ∀a b. coprime a b ⇒ ∀n. coprime a (b ** n)
   
   [coprime_factor_coprime]  Theorem
      
      ⊢ ∀m n. m divides n ⇒ ∀k. coprime n k ⇒ coprime m k
   
   [coprime_factor_not_divides]  Theorem
      
      ⊢ ∀n k.
          1 < n ∧ coprime n k ⇒ ∀p. 1 < p ∧ p divides n ⇒ ¬(p divides k)
   
   [coprime_gt_1]  Theorem
      
      ⊢ ∀n k. coprime k n ∧ 1 < n ⇒ 0 < k
   
   [coprime_mod]  Theorem
      
      ⊢ ∀m n. 0 < m ∧ coprime m n ⇒ coprime m (n MOD m)
   
   [coprime_mod_iff]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ (coprime m n ⇔ coprime m (n MOD m))
   
   [coprime_neq_1]  Theorem
      
      ⊢ ∀n k. coprime k n ∧ n ≠ 1 ⇒ k ≠ 0
   
   [coprime_prime_factor_coprime]  Theorem
      
      ⊢ ∀n p. 1 < n ∧ prime p ∧ p divides n ⇒ ∀k. coprime n k ⇒ coprime p k
   
   [coprime_product_coprime]  Theorem
      
      ⊢ ∀x y z. coprime x z ∧ coprime y z ⇒ coprime (x * y) z
   
   [coprime_product_coprime_iff]  Theorem
      
      ⊢ ∀x y z. coprime x z ⇒ (coprime y z ⇔ coprime (x * y) z)
   
   [coprime_product_coprime_sym]  Theorem
      
      ⊢ ∀x y z. coprime z x ∧ coprime z y ⇒ coprime z (x * y)
   
   [coprime_product_divides]  Theorem
      
      ⊢ ∀n a b. a divides n ∧ b divides n ∧ coprime a b ⇒ a * b divides n
   
   [coprime_sym]  Theorem
      
      ⊢ ∀x y. coprime x y ⇔ coprime y x
   
   [divides_coprime_mul]  Theorem
      
      ⊢ ∀n m k. coprime n m ⇒ (n divides m * k ⇔ n divides k)
   
   [divides_iff_gcd_fix]  Theorem
      
      ⊢ ∀m n. n divides m ⇔ gcd n m = n
   
   [divides_iff_lcm_fix]  Theorem
      
      ⊢ ∀m n. n divides m ⇔ lcm n m = m
   
   [divides_imp_coprime_with_predecessor]  Theorem
      
      ⊢ ∀m n. 0 < m ∧ n divides m ⇒ coprime n (PRE m)
   
   [divides_imp_coprime_with_successor]  Theorem
      
      ⊢ ∀m n. n divides m ⇒ coprime n (SUC m)
   
   [gcd_LESS_EQ]  Theorem
      
      ⊢ ∀m n. n ≠ 0 ⇒ gcd m n ≤ n
   
   [gcd_compute]  Theorem
      
      ⊢ (∀y. gcd 0 y = y) ∧
        (∀x. gcd <..num comp'n..> 0 = <..num comp'n..> ) ∧
        (∀x. gcd <..num comp'n..> 0 = <..num comp'n..> ) ∧
        (∀y x.
           gcd <..num comp'n..> <..num comp'n..> =
           if <..num comp'n..> − 1 ≤ <..num comp'n..> − 1 then
             gcd (<..num comp'n..> − 1 − (<..num comp'n..> − 1))
               <..num comp'n..>
           else
             gcd <..num comp'n..>
               (<..num comp'n..> − 1 − (<..num comp'n..> − 1))) ∧
        (∀y x.
           gcd <..num comp'n..> <..num comp'n..> =
           if <..num comp'n..> − 1 ≤ <..num comp'n..> then
             gcd (<..num comp'n..> − (<..num comp'n..> − 1))
               <..num comp'n..>
           else
             gcd <..num comp'n..>
               (<..num comp'n..> − 1 − <..num comp'n..> )) ∧
        (∀y x.
           gcd <..num comp'n..> <..num comp'n..> =
           if <..num comp'n..> ≤ <..num comp'n..> − 1 then
             gcd (<..num comp'n..> − 1 − <..num comp'n..> )
               <..num comp'n..>
           else
             gcd <..num comp'n..>
               (<..num comp'n..> − (<..num comp'n..> − 1))) ∧
        ∀y x.
          gcd <..num comp'n..> <..num comp'n..> =
          if <..num comp'n..> ≤ <..num comp'n..> then
            gcd (<..num comp'n..> − <..num comp'n..> ) <..num comp'n..>
          else gcd <..num comp'n..> (<..num comp'n..> − <..num comp'n..> )
   
   [gcd_coprime_cancel]  Theorem
      
      ⊢ ∀m n p. coprime p n ⇒ gcd (p * m) n = gcd m n
   
   [gcd_def]  Theorem
      
      ⊢ (∀y. gcd 0 y = y) ∧ (∀x. gcd (SUC x) 0 = SUC x) ∧
        ∀y x.
          gcd (SUC x) (SUC y) =
          if y ≤ x then gcd (x − y) (SUC y) else gcd (SUC x) (y − x)
   
   [gcd_ind]  Theorem
      
      ⊢ ∀P. (∀y. P 0 y) ∧ (∀x. P (SUC x) 0) ∧
            (∀x y.
               (¬(y ≤ x) ⇒ P (SUC x) (y − x)) ∧ (y ≤ x ⇒ P (x − y) (SUC y)) ⇒
               P (SUC x) (SUC y)) ⇒
            ∀v v1. P v v1
   
   [prime_not_coprime_divides]  Theorem
      
      ⊢ ∀n p. prime p ∧ gcd p n ≠ 1 ⇒ p divides n
   
   [prime_not_divides_coprime]  Theorem
      
      ⊢ ∀n p. prime p ∧ ¬(p divides n) ⇒ coprime p n
   
   [primes_coprime]  Theorem
      
      ⊢ ∀p q. prime p ∧ prime q ∧ p ≠ q ⇒ coprime p q
   
   
*)
end

HOL 4, Trindemossen-2