# 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.

Solution
## Notes

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