proposition: Lemma Qmult_integral : forall q r, q * r == 0 -> q == 0 \/ r == 0.
proof: Proof. intros. destruct (Qeq_dec q 0)%Q. - left ; apply q0. - apply Qmult_integral_l in H ; tauto. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant