Example of a ring: 〈Q,[+],[*]〉Because Q forms an abelian group with addition, a monoid with multiplication and it satisfies the distributive law, it is a ring.
Lemma Q_mult_plus_is_dist : distributive Qmult_is_bin_fun Qplus_is_bin_fun.
Definition Q_is_CRing : is_CRing Q_as_CAbGroup 1 Qmult_is_bin_fun.
Definition Q_as_CRing := Build_CRing _ _ _ Q_is_CRing.
Canonical Structure Q_as_CRing.
The following lemmas are used in the proof that Q is Archimeadian.