The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi all!

1/ I don't remember the Internet tool to chat with Coq users, to ask
   simple questions. I used it once a long time ago, but I did not
   notice what I used, and I cannot find it again through google.

2/ The immediate question that I have now is how to prove that the
   hypothesis (1 / 3)%R = 1%R is contradictory? I tried discriminate,
   discrR and other field_simplify. But I cannot manage to finish it
   in a simple way. A research on google gave me nothing interesting
   but perhaps I did not put the good terms.

Thanks.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/