proposition: Lemma second_Q_Ring_Theory : ring_theory Zero Qone Qplus_lazy Qmult_lazy Qminus_lazy Qopp_lazy (eq(A:=Q)).
proof: Proof. split; intros n m p || intros n m || intros n; repeat rewrite Qplus_lazy_Qplus; repeat rewrite Qmult_lazy_Qmult; repeat rewrite Qminus_lazy_Qminus; repeat rewrite Qdiv_lazy_Qdiv; repeat rewrite Qopp_lazy_Qopp; repeat rewrite Qinv_lazy_Qinv; try 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)