proposition: Lemma second_QField : field_theory Zero Qone Qplus_lazy Qmult_lazy Qminus_lazy Qopp_lazy total_Qdiv_lazy total_Qinv_lazy (eq(A:=Q)).
proof: Proof. constructor. apply second_Q_Ring_Theory. discriminate. intros; unfold total_Qdiv_lazy, total_Qinv_lazy in |- *. destruct (Q_zerop q). rewrite Qmult_lazy_Qmult in |- *. ring. rewrite Qdiv_lazy_Qdiv in |- *; rewrite Qmult_lazy_Qmult in |- *; rewrite Qinv_lazy_Qinv in |- *; reflexivity. exact total_Qinv_lazy_defT. Defined.
imports: Coq(Eqdep_dec)