The Coq mailing list

[Dimitri Hendriks <diem AT xs4all.nl>]

Hi,

I need a notion of relative primality on natural numbers, and thought the 
library NPeano would be useful.
I do not want to look into the specific details on the implementation of gcd, 
and would like basic lemmas 
(like gcd a (a + b) = gcd a b) to be proved automatically. Is there a hints 
database for doing that with auto,
are there other useful tactics, or how would you proceed? Am I better off 
defining things from scratch?

Thanks, 
Dimitri