proposition: Lemma Q2R_mult : forall x y : Q, Q2R (x*y) = (Q2R x * Q2R y)%R.
proof: Proof. unfold Qmult, Qeq, Q2R; intros (x1, x2) (y1, y2); unfold Qden, Qnum. simpl_mult. do 2 rewrite mult_IZR. field; auto. Qed.
imports: Rdefinitions Raxioms RIneq QArith_base