Lemma ap_Q_irreflexive1 : irreflexive (A:=Q) Qap.

Lemma ap_Q_symmetric1 : Csymmetric Qap.

Lemma ap_Q_cotransitive1 : cotransitive (A:=Q) Qap.

Lemma ap_Q_tight1 : tight_apart (A:=Q) Qeq Qap.

Definition ap_Q_is_apartness := Build_is_CSetoid Q Qeq Qap
 ap_Q_irreflexive1 ap_Q_symmetric1 ap_Q_cotransitive1 ap_Q_tight1.

Definition Q_as_CSetoid := Build_CSetoid _ _ _ ap_Q_is_apartness.
Canonical Structure Q_as_CSetoid.
Canonical Structure Q_is_Setoid := (cs_crr Q_as_CSetoid).

Lemma Qplus_wd : bin_fun_wd Q_as_CSetoid Q_as_CSetoid Q_as_CSetoid Qplus.

Lemma Qplus_strext1 : bin_fun_strext Q_as_CSetoid Q_as_CSetoid Q_as_CSetoid Qplus.

Definition Qplus_is_bin_fun := Build_CSetoid_bin_fun _ _ _ _ Qplus_strext1.
Canonical Structure Qplus_is_bin_fun.

Lemma Qplus_is_assoc : associative Qplus_is_bin_fun.

Lemma Qplus_is_commut1 : commutes Qplus_is_bin_fun.

Lemma Qopp_wd : fun_wd (S1:=Q_as_CSetoid) (S2:=Q_as_CSetoid) Qopp.

Lemma Qopp_strext : fun_strext (S1:=Q_as_CSetoid) (S2:=Q_as_CSetoid) Qopp.

Definition Qopp_is_fun := Build_CSetoid_fun _ _ _ Qopp_strext.
Canonical Structure Qopp_is_fun.

Lemma Qmult_wd : bin_fun_wd Q_as_CSetoid Q_as_CSetoid Q_as_CSetoid Qmult.

Lemma Qmult_strext1 : bin_fun_strext Q_as_CSetoid Q_as_CSetoid Q_as_CSetoid Qmult.

Definition Qmult_is_bin_fun := Build_CSetoid_bin_fun _ _ _ _ Qmult_strext1.
Canonical Structure Qmult_is_bin_fun.

Lemma Qmult_is_assoc : associative Qmult_is_bin_fun.

Lemma Qmult_is_commut : commutes Qmult_is_bin_fun.

Lemma Qlt_strext : Crel_strext Q_as_CSetoid Qlt.

Definition Qlt_is_CSetoid_relation := Build_CCSetoid_relation _ _ Qlt_strext.
Canonical Structure Qlt_is_CSetoid_relation.