About the danger of axioms

Consider the following definition of positive rational numbers, including an axiom stating that if ad=bc, then a/b=c/d.
Show that this theory is unconsistent.


We hope that this exercise will warn you against the danger of putting axioms in your theories. If you don't leave your Coq session immediately, please type the following command :
Reset eq_RatPlus.
to get a consistent environment.

A possible way to get a theory of rational numbers is to replace Coq's equality by an equivalence relation. Please look at Setoids in Coq's documentation.

Going home
Pierre Castéran