GCD and mod in Coq

Question

I'm stuck at a problem in Coq, would be great if anyone had any tips on how to break the problem down into smaller steps. The lemma is this:

Lemma gcd_prime : forall (a b : Z), a > 1 -> b > 1 -> 
  Z.gcd a b = 1 -> Zmod a b <> 0

That is, if a and b are coprime and higher than 1, a mod b is not 0.

This is where I'm stuck:

 p : positive
 p0 : positive
 H : Z.pos p > 1
 H0 : Z.pos p0 > 1
 H1 : Z.gcd (Z.pos p) (Z.pos p0) = 1
  ============================
  Z.pos p mod Z.pos p0 <> 0

After doing the intros and induction and removed the obvious cases.

Maybe I must rephrase the mod part into remainder instead? Or should I replace H1 with something weaker, like p <> p0?

Doing SearchAbout Zmod. returns a lot of lemmas, but I'm not sure on how to adapt them.

Regards

Olle

Answer 1

SearchAbout and omega are your friends. Remember you can search things that mention several definitions at once, such as Z.gcd and 0. Here's a solution:

Require Import ZArith.

Open Scope Z_scope.

Lemma gcd_prime : forall (a b : Z), a > 1 -> b > 1 ->
  Z.gcd a b = 1 -> Zmod a b <> 0.
Proof.
  intros a b Ha Hb Hgcd Hmod.
  rewrite (Z_div_mod_eq a b), Hmod, Zplus_0_r in Hgcd; try omega.
  rewrite Z.gcd_comm, Z.gcd_mul_diag_l in Hgcd; omega.
Qed.