proposition: Lemma Q_Ring_Theory : ring_theory Zero Qone Qplus Qmult Qminus Qopp (eq(A:=Q)).
proof: Proof. split; intros n m p || intros n m || intros n; solve [ first [ apply Qplus_sym | apply Qplus_assoc | apply Qmult_sym | apply Qmult_assoc | apply Qplus_zero_left | apply Qmult_one_left | apply Q_opp_def | apply Q_distr_left | reflexivity ]]. Defined.
imports: Coq(Eqdep_dec)