title: How to prove that a number is prime using Znumtheory in Coq
body: <p>I'm trying to prove that a number is prime using the Znumtheory library.</p>
  
  <p>In Znumtheory primes are defined in terms of relative primes: </p>
  
  <pre><code>  Inductive prime (p:Z) : Prop :=
        prime_intro :
        1 &lt; p -&gt; (forall n:Z, 1 &lt;= n &lt; p -&gt; rel_prime n p) -&gt; prime p.
  </code></pre>
  
  <p>So to prove that 3 is prime I should apply prime_intro to the goal. Here is my try:</p>
  
  <pre><code>Theorem prime3 : prime 3.
  Proof.
      apply prime_intro.
  
    - omega.
    - intros. 
      unfold rel_prime. apply Zis_gcd_intro.
      + apply Z.divide_1_l.
      + apply Z.divide_1_l.
      + intros. Abort.
  </code></pre>
  
  <p>I don't know how to use the hypothesis <code>H : 1 &lt;= n &lt; 3</code> which says that <code>n</code> is <code>1</code> or <code>2</code>. I could destruct it, apply <code>lt_eq_cases</code> and destruct it again, but I would be stuck with a useless <code>1 &lt; n</code> in the first case.</p>
  
  <p>I wasn't expecting to have a hard time with something that looks so simple.</p>